@@ -203,7 +203,8 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
203 case lookupCtxtExact n (idris_datatypes ist) of
203 case lookupCtxtExact n (idris_datatypes ist) of
204 Just t -> do
204 Just t -> do
205 let others = hints ++ con_names t ++ autohints
205 let others = hints ++ con_names t ++ autohints
206+ when (not fromProver && length (con_names t) > 1)
206− when (not fromProver) -- in interactive mode,
207+ -- in interactive mode,
207 -- don't just guess (fine for 'auto',
208 -- don't just guess (fine for 'auto',
208 -- since that's part of the point...)
209 -- since that's part of the point...)
209 $ checkConstructor ist others
210 $ checkConstructor ist others