@@ -201,11 +201,13 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
201201 Nothing -> []
202202 Just hs -> hs
203203 case lookupCtxtExact n (idris_datatypes ist) of
204− Just t -> tryCons d locs tys
205− (hints ++
206− con_names t ++
207− autohints ++
208− getFn d fn)
204+ Just t -> do
205+ let others = hints ++ con_names t ++ autohints
206+ when (not fromProver) -- in interactive mode,
207+ -- don't just guess (fine for 'auto',
208+ -- since that's part of the point...)
209+ $ checkDisjoint ist [] others
210+ tryCons d locs tys (others ++ getFn d fn)
209211 Nothing -> fail "Not a data type"
210212 _ -> fail "Not a data type"
211213
@@ -221,15 +223,9 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
221223 | otherwise = try' (tryLocal d (x : locs) tys x t)
222224 (tryLocals d locs tys xs) True
223225
224− tryCons d locs tys cs = do when (not fromProver) -- in interactive mode,
225− -- don't just guess (fine for 'auto',
226− -- since that's part of the point...)
227− $ checkDisjoint ist [] cs
228− tryCons' d locs tys cs
229−
230− tryCons' d locs tys [] = fail "Constructors failed"
231− tryCons' d locs tys (c : cs)
232− = try' (tryCon d locs tys c) (tryCons' d locs tys cs) True
226+ tryCons d locs tys [] = fail "Constructors failed"
227+ tryCons d locs tys (c : cs)
228+ = try' (tryCon d locs tys c) (tryCons d locs tys cs) True
233229
234230 tryLocal d locs tys n t
235231 = do let a = getPArity (delab ist (binderTy t))