Ajout erreur DoesNotOccurIn

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1067 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 17 insertions, 2 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 8021f336e..58fb8490e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -21,14 +21,19 @@ open Retyping
 open Evarutil
 
 type refiner_error =
+
+  (* Errors raised by the refiner *)
   | BadType of constr * constr * constr
   | OccurMeta of constr
   | CannotApply of constr * constr
+  | NotWellTyped of constr
+
+  (* Errors raised by the tactics *)
   | CannotUnify of constr * constr
   | CannotGeneralize of constr
-  | NotWellTyped of constr
   | BadTacticArgs of string * tactic_arg list
   | IntroNeedsProduct
+  | DoesNotOccurIn of constr * identifier
 
 exception RefinerError of refiner_error
 
diff --git a/proofs/logic.mli b/proofs/logic.mli
index eade902ba..1038b5c0d 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -36,14 +36,19 @@ val prim_extractor :
 (*s Refiner errors. *)
 
 type refiner_error =
+
+  (*i Errors raised by the refiner i*)
   | BadType of constr * constr * constr
   | OccurMeta of constr
   | CannotApply of constr * constr
+  | NotWellTyped of constr
+
+  (*i Errors raised by the tactics i*)
   | CannotUnify of constr * constr
   | CannotGeneralize of constr
-  | NotWellTyped of constr
   | BadTacticArgs of string * tactic_arg list
   | IntroNeedsProduct
+  | DoesNotOccurIn of constr * identifier
 
 exception RefinerError of refiner_error
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 83da9abef..57b2c2ac8 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