diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-21 11:51:33 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-21 11:51:33 +0000 |
| commit | 0dece739c580b39d77708bb8117442e7e1cd560b (patch) | |
| tree | 3db834fd12224590c4feddd213a41a0edd7c4986 /toplevel | |
| parent | 094b40758cb4278b33a87e5633cf4ac716f348b4 (diff) | |
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3474 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index c3be3d98a..46cadeb0a 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -416,12 +416,18 @@ let explain_refiner_cannot_applt t harg = prterm t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++ prterm harg -let explain_refiner_cannot_unify m n = +let explain_cannot_unify m n = let pm = prterm m in let pn = prterm n in str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ str"with" ++ brk(1,1) ++ pn +let explain_cannot_unify_binding_type m n = + let pm = prterm m in + let pn = prterm n in + str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ + str "which should be unifiable with" ++ brk(1,1) ++ pn + let explain_refiner_cannot_generalize ty = str "Cannot find a well-typed generalisation of the goal with type : " ++ prterm ty @@ -440,17 +446,22 @@ let explain_non_linear_proof c = str "cannot refine with term" ++ brk(1,1) ++ prterm c ++ spc () ++ str"because a metavariable has several occurrences" +let explain_no_occurrence_found c = + str "Found no subterm matching " ++ prterm c ++ str " in the current goal" + let explain_refiner_error = function | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty | OccurMeta t -> explain_refiner_occur_meta t | OccurMetaGoal t -> explain_refiner_occur_meta_goal t | CannotApply (t,harg) -> explain_refiner_cannot_applt t harg - | CannotUnify (m,n) -> explain_refiner_cannot_unify m n + | CannotUnify (m,n) -> explain_cannot_unify m n + | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type m n | CannotGeneralize ty -> explain_refiner_cannot_generalize ty | NotWellTyped c -> explain_refiner_not_well_typed c | IntroNeedsProduct -> explain_intro_needs_product () | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp | NonLinearProof c -> explain_non_linear_proof c + | NoOccurrenceFound c -> explain_no_occurrence_found c (* Inductive errors *) |