diff options
| author | herbelin | 2000-12-06 11:39:45 +0000 |
|---|---|---|
| committer | herbelin | 2000-12-06 11:39:45 +0000 |
| commit | 10efe99cd5d19ad5e643b50234e38a8384f0657f (patch) | |
| tree | c12e56139aa6770c148389297c57eb9b1ecbca97 /toplevel | |
| parent | c72588e26c59037fe9a9455f9796c0dfd5bc9ed1 (diff) | |
Ajout erreur DoesNotOccurIn
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1067 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 83da9abef8..57b2c2ac85 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -414,6 +414,10 @@ let explain_refiner_bad_tactic_args s l = let explain_intro_needs_product () = [< 'sTR "Introduction tactics needs products" >] +let explain_does_not_occur_in c hyp = + [< 'sTR "The term"; 'sPC; prterm c; 'sPC; 'sTR "does not occur in"; + 'sPC; pr_id hyp >] + let explain_refiner_error = function | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty | OccurMeta t -> explain_refiner_occur_meta t @@ -423,6 +427,7 @@ let explain_refiner_error = function | NotWellTyped c -> explain_refiner_not_well_typed c | BadTacticArgs (s,l) -> explain_refiner_bad_tactic_args s l | IntroNeedsProduct -> explain_intro_needs_product () + | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp let error_non_strictly_positive k env c v = let pc = prterm_env env c in |