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

16 files changed, 88 insertions, 68 deletions

diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 469a067f44..bc9f706c57 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -196,7 +196,7 @@ let make_pbp_atomic_tactic = function
   | PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
   | PbpApply h -> TacAtom (zz, TacApply (make_var h,NoBindings))
   | PbpElim (hyp_name, names) ->
-      let bind = List.map (fun s -> (NamedHyp s,make_pbp_pattern s)) names in
+      let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in
       TacAtom
 	(zz, TacElim ((make_var hyp_name,ExplicitBindings bind),None))
   | PbpTryClear l -> 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 0d3739636e..272ca09f50 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -413,7 +413,7 @@ let xlate_quantified_hypothesis_opt = function
   | Some (AnonHyp n) -> xlate_int_to_id_or_int_opt n
   | Some (NamedHyp id) -> xlate_id_to_id_or_int_opt id;;
 
-let xlate_explicit_binding (h,c) = 
+let xlate_explicit_binding (loc,h,c) = 
   CT_binding (xlate_quantified_hypothesis h, xlate_formula c)
 
 let xlate_bindings = function
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 5cfc324eb7..c7f8217d1f 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -47,28 +47,9 @@ let local_compute =
     Qast.Node ("FIota", []);
     Qast.Node ("FZeta", [])]
 
-(*
-  let
-    {rBeta = b; rIota = i; rZeta = z; rDelta = d; rConst = l} = make_red_flag s
-  in
-  let quotify_ident id =
-    Qast.Apply ("Names.id_of_string", [Qast.Str (Names.string_of_id id)])
-  in
-  let quotify_path sp =
-    let dir, id = Names.repr_path sp in
-    let l = Names.repr_dirpath dir in
-    Qast.Apply ("Names.make_path",
-      [Qast.Apply ("Names.make_dirpath",
-        [Qast.List (List.map quotify_ident l)]);
-      quotify_ident id]) in
-  Qast.Record 
-    ["rBeta",Qast.Bool b; "rIota",Qast.Bool i;
-     "rZeta",Qast.Bool z; "rDelta",Qast.Bool d;
-     "rConst",Qast.List (List.map quotify_path l)]
-*)
 ifdef Quotify then open Q
 
-(* Please leave several GEXTEND for modular compilation under PowerPC *)
+let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 
 (* Auxiliary grammar rules *)
 
@@ -169,14 +150,15 @@ GEXTEND Gram
       ] ]
   ;
   simple_binding:
-    [ [ id = base_ident; ":="; c = constr -> (NamedHyp id, c)
-      | n = natural; ":="; c = constr -> (AnonHyp n, c) ] ]
+    [ [ id = base_ident; ":="; c = constr -> (loc, NamedHyp id, c)
+      | n = natural; ":="; c = constr -> (loc, AnonHyp n, c) ] ]
   ;
   binding_list:
     [ [ c1 = constr; ":="; c2 = constr; bl = LIST0 simple_binding ->
-          ExplicitBindings ((NamedHyp (coerce_to_id c1), c2) :: bl)
+          ExplicitBindings
+            ((join_to_constr loc c2,NamedHyp (coerce_to_id c1), c2) :: bl)
       | n = natural; ":="; c = constr; bl = LIST0 simple_binding ->
-	  ExplicitBindings ((AnonHyp n, c) :: bl)
+	  ExplicitBindings ((join_to_constr loc c,AnonHyp n, c) :: bl)
       | c1 = constr; bl = LIST0 constr ->
 	  ImplicitBindings (c1 :: bl) ] ]
   ;
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 6c45c9e70a..c44881614e 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -75,8 +75,8 @@ let pr_quantified_hypothesis = function
 let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h
 
 let pr_binding prc = function
-  | NamedHyp id, c -> hov 1 (pr_id id ++ str ":=" ++ cut () ++ prc c)
-  | AnonHyp n, c -> hov 1 (int n ++ str ":=" ++ cut () ++ prc c)
+  | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str ":=" ++ cut () ++ prc c)
+  | loc, AnonHyp n, c -> hov 1 (int n ++ str ":=" ++ cut () ++ prc c)
 
 let pr_bindings prc = function
   | ImplicitBindings l ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index bc8128fd85..1f352f6af1 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -159,6 +159,8 @@ let mlexpr_of_quantified_hypothesis = function
 
 let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >>
 
+let mlexpr_of_loc loc = <:expr< $dloc$ >>
+
 let mlexpr_of_hyp_location = function
   | Tacexpr.InHyp id ->
       <:expr< Tacexpr.InHyp $mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident) id$ >>
@@ -268,7 +270,7 @@ let rec mlexpr_of_may_eval f = function
 
 let mlexpr_of_binding_kind = function
   | Rawterm.ExplicitBindings l ->
-      let l = mlexpr_of_list (mlexpr_of_pair mlexpr_of_quantified_hypothesis mlexpr_of_constr) l in
+      let l = mlexpr_of_list (mlexpr_of_triple mlexpr_of_loc mlexpr_of_quantified_hypothesis mlexpr_of_constr) l in
       <:expr< Rawterm.ExplicitBindings $l$ >>
   | Rawterm.ImplicitBindings l -> 
       let l = mlexpr_of_list mlexpr_of_constr l in
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 9354035497..8ea4a25c3d 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -35,7 +35,7 @@ type binder_kind = BProd | BLambda | BLetIn
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
 
-type 'a explicit_substitution = (quantified_hypothesis * 'a) list
+type 'a explicit_substitution = (loc * quantified_hypothesis * 'a) list
 
 type 'a substitution = 
   | ImplicitBindings of 'a list
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 3c2241682b..981cb23314 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -35,7 +35,7 @@ type binder_kind = BProd | BLambda | BLetIn
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
 
-type 'a explicit_substitution = (quantified_hypothesis * 'a) list
+type 'a explicit_substitution = (loc * quantified_hypothesis * 'a) list
 
 type 'a substitution = 
   | ImplicitBindings of 'a list
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 77aa72439f..3ab1dbdd48 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -75,7 +75,6 @@ type 'a freelisted = {
   rebus : 'a;
   freemetas : Intset.t }
 
-
 (* collects all metavar occurences, in left-to-right order, preserving
  * repetitions and all. *)
 
@@ -122,7 +121,7 @@ type wc = named_context sigma
 let mentions clenv mv0 = 
   let rec menrec mv1 =
     try
-      (match Intmap.find mv1 clenv.env with
+     (match Intmap.find mv1 clenv.env with
 	 | Clval (b,_) -> 
 	     Intset.mem mv0 b.freemetas || intset_exists menrec b.freemetas
 	 | Cltyp _ -> false)
@@ -729,23 +728,30 @@ let unify_to_subterm clause (op,cl) =
           | _ -> error "Match_subterm")) 
   in 
   if isMeta op then error "Match_subterm";
-  matchrec cl
+  try matchrec cl
+  with ex when catchable_exception ex ->
+    raise (RefinerError (NoOccurrenceFound op))
 
 (* Possibly gives K-terms in case the operator does not contain 
    a meta : BUG ?? *)
 let unify_to_subterm_list allow_K clause oplist t = 
   List.fold_right 
     (fun op (clause,l) -> 
-       if occur_meta op then 
+       if occur_meta op then
          let (clause',cl) =
-           (try 
-	      unify_to_subterm clause (strip_outer_cast op,t)
-            with e when catchable_exception e ->
-              if allow_K then (clause,op) else raise e)
+           try 
+	     (* This is up to some delta ... *)
+	     unify_to_subterm clause (strip_outer_cast op,t)
+           with RefinerError (NoOccurrenceFound _) when allow_K -> (clause,op)
          in 
 	 (clause',cl::l)
-       else 
-	 (clause,op::l)) 
+       else
+	 if not allow_K & not (dependent op t) then
+	   (* This is not up to delta ... *)
+	   raise (RefinerError (NoOccurrenceFound op))
+	 else
+	 (* Optimisation *)
+	 (clause,op::l))
     oplist 
     (clause,[])
 
@@ -808,17 +814,19 @@ let clenv_unify allow_K cv_pb ty1 ty2 clenv =
 	 with ex when catchable_exception ex -> 
 	   try 
 	     clenv_unify2 allow_K cv_pb ty1 ty2 clenv
-	   with ex when catchable_exception ex -> 
+	   with RefinerError (NoOccurrenceFound c) as e -> raise e
+	     | ex when catchable_exception ex -> 
 	     error "Cannot solve a second-order unification problem")
 
      (* Second order case *)
      | (Meta _, true, _, _ | _, _, Meta _, true) -> 
 	(try 
 	   clenv_unify2 allow_K cv_pb ty1 ty2 clenv
-         with ex when catchable_exception ex -> 
-           try 
+	with RefinerError (NoOccurrenceFound c) as e -> raise e
+	  | ex when catchable_exception ex -> 
+          try 
 	     clenv_typed_unify cv_pb ty1 ty2 clenv
-           with ex when catchable_exception ex -> 
+          with ex when catchable_exception ex -> 
              error "Cannot solve a second-order unification problem")
 
      (* General case: try first order *)
@@ -994,20 +1002,21 @@ let clenv_match_args s clause =
   let mvs = clenv_independent clause in 
   let rec matchrec clause = function
     | [] -> clause
-    | (b,c)::t ->
+    | (loc,b,c)::t ->
 	let k =
 	  match b with
             | NamedHyp s ->
-		if List.mem_assoc b t then 
+		if List.exists (fun (_,b',_) -> b=b') t then 
 		  errorlabstrm "clenv_match_args" 
 		    (str "The variable " ++ pr_id s ++ 
 		    str " occurs more than once in binding")
 		else
 		  clenv_lookup_name clause s
 	    | AnonHyp n ->
-		if List.mem_assoc b t then errorlabstrm "clenv_match_args"
-		  (str "The position " ++ int n ++
-		  str " occurs more than once in binding");
+		if List.exists (fun (_,b',_) -> b=b') t then
+		  errorlabstrm "clenv_match_args"
+		    (str "The position " ++ int n ++
+		    str " occurs more than once in binding");
 		try 
 		  List.nth mvs (n-1)
 		with (Failure _|Invalid_argument _) ->
@@ -1026,7 +1035,10 @@ let clenv_match_args s clause =
 	  (* Try to coerce to the type of [k]; cannot merge with the
 	     previous case because Coercion does not handle Meta *)
           let c' = w_coerce clause.hook c c_typ k_typ in
-	  clenv_unify true CONV (mkMeta k) c' clause
+	  try clenv_unify true CONV (mkMeta k) c' clause
+	  with RefinerError (CannotUnify (m,n)) ->
+	    Stdpp.raise_with_loc loc
+ 	      (RefinerError (CannotUnifyBindingType (m,n)))
 	in matchrec cl t
   in 
   matchrec clause s
@@ -1082,6 +1094,14 @@ let clenv_pose_dependent_evars clenv =
 
 (***************************)
 
+let is_dependent clause =
+  match
+    kind_of_term (clenv_instance_template clause),
+    kind_of_term (clenv_instance_template_type clause)
+  with
+      App(f,l), App(g,l') when isMeta g & array_last l = array_last l' -> true
+    | _ -> false
+
 let clenv_unique_resolver allow_K clause gl =
   clenv_unify allow_K CUMUL
     (clenv_instance_template_type clause) (pf_concl gl) clause 
@@ -1092,8 +1112,8 @@ let res_pf kONT clenv gls =
 let res_pf_cast kONT clenv gls =
   clenv_refine_cast kONT (clenv_unique_resolver false clenv gls) gls
 
-let elim_res_pf kONT clenv gls =
-  clenv_refine_cast kONT (clenv_unique_resolver true clenv gls) gls
+let elim_res_pf kONT clenv allow_K gls =
+  clenv_refine_cast kONT (clenv_unique_resolver allow_K clenv gls) gls
 
 let elim_res_pf_THEN_i kONT clenv tac gls =  
   let clenv' = (clenv_unique_resolver true clenv gls) in
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index c056c3b2c8..3e39fc3e6c 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -113,7 +113,7 @@ val unify : constr -> tactic
 val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic
 val res_pf      : (wc -> tactic) -> wc clausenv -> tactic
 val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic
-val elim_res_pf : (wc -> tactic) -> wc clausenv -> tactic
+val elim_res_pf : (wc -> tactic) -> wc clausenv -> bool -> tactic
 val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic
 val elim_res_pf_THEN_i : 
   (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic array) -> tactic
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5c95a8e7a4..da62c1036c 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -42,9 +42,11 @@ type refiner_error =
 
   (* Errors raised by the tactics *)
   | CannotUnify of constr * constr
+  | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
   | IntroNeedsProduct
   | DoesNotOccurIn of constr * identifier
+  | NoOccurrenceFound of constr
 
 exception RefinerError of refiner_error
 
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 7d449c71d8..6eedb1ba05 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -55,9 +55,11 @@ type refiner_error =
 
   (*i Errors raised by the tactics i*)
   | CannotUnify of constr * constr
+  | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
   | IntroNeedsProduct
   | DoesNotOccurIn of constr * identifier
+  | NoOccurrenceFound of constr
 
 exception RefinerError of refiner_error
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4fc8c04e16..494cb50456 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -71,7 +71,7 @@ let general_rewrite_bindings lft2rgt (c,l) gl =
           else
 	    pf_global gl (id_of_string (hdcncls^suffix))
         in 
-	tclNOTSAMEGOAL (general_elim (c,l) (elim,NoBindings)) gl
+	tclNOTSAMEGOAL (general_elim (c,l) (elim,NoBindings) ~allow_K:false) gl
    (* was tclWEAK_PROGRESS which only fails for tactics generating one subgoal 
       and did not fail for useless conditional rewritings generating an
       extra condition *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 05b26cbb64..64bf9371fd 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -353,8 +353,8 @@ let glob_constr ist c =
   in c
 
 (* Globalize bindings *)
-let glob_binding ist (b,c) =
-  (glob_quantified_hypothesis ist b,glob_constr ist c)
+let glob_binding ist (loc,b,c) =
+  (loc,glob_quantified_hypothesis ist b,glob_constr ist c)
 
 let glob_bindings ist = function
   | NoBindings -> NoBindings
@@ -1065,8 +1065,8 @@ let interp_induction_arg ist = function
 (*	    (constr_interp ist (Termast.ast_of_qualid (make_short_qualid id)))*)
 	    (constr_interp ist (CRef (Ident (loc,id))))
 
-let binding_interp ist (b,c) =
-  (interp_quantified_hypothesis ist b,constr_interp ist c)
+let binding_interp ist (loc,b,c) =
+  (loc,interp_quantified_hypothesis ist b,constr_interp ist c)
 
 let bindings_interp ist = function
   | NoBindings -> NoBindings
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e72a35ab4a..eb1829bf6a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -859,7 +859,7 @@ let last_arg c = match kind_of_term c with
   | App (f,cl) ->  array_last cl
   | _ -> anomaly "last_arg"
 	
-let elimination_clause_scheme kONT elimclause indclause gl = 
+let elimination_clause_scheme kONT elimclause indclause allow_K gl = 
   let indmv = 
     (match kind_of_term (last_arg (clenv_template elimclause).rebus) with
        | Meta mv -> mv
@@ -867,7 +867,7 @@ let elimination_clause_scheme kONT elimclause indclause gl =
              (str "The type of elimination clause is not well-formed")) 
   in
   let elimclause' = clenv_fchain indmv elimclause indclause in 
-  elim_res_pf kONT elimclause' gl
+  elim_res_pf kONT elimclause' allow_K gl
 
 (* cast added otherwise tactics Case (n1,n2) generates (?f x y) and 
  * refine fails *)
@@ -883,14 +883,14 @@ let type_clenv_binding wc (c,t) lbind =
  * matching I, lbindc are the expected terms for c arguments 
  *)
 
-let general_elim (c,lbindc) (elimc,lbindelimc) gl = 
+let general_elim (c,lbindc) (elimc,lbindelimc) ?(allow_K=true) gl = 
   let (wc,kONT)  = startWalk gl in
   let ct = pf_type_of gl c in
   let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
   let indclause  = make_clenv_binding wc (c,t) lbindc  in
   let elimt      = w_type_of wc elimc in
   let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in 
-  elimination_clause_scheme kONT elimclause indclause gl
+  elimination_clause_scheme kONT elimclause indclause allow_K gl
 
 (* Elimination tactic with bindings but using the default elimination 
  * constant associated with the type. *)
@@ -1251,7 +1251,7 @@ let induction_tac varname typ (elimc,elimt,lbindelimc) gl =
   let indclause  = make_clenv_binding wc (c,typ) NoBindings  in
   let elimclause =
     make_clenv_binding wc (mkCast (elimc,elimt),elimt) lbindelimc in
-  elimination_clause_scheme kONT elimclause indclause gl
+  elimination_clause_scheme kONT elimclause indclause true gl
 
 let compute_induction_names n names =
   let names = if names = [] then Array.make n [] else Array.of_list names in
@@ -1437,7 +1437,7 @@ let elim_scheme_type elim t gl =
         let clause' =
 	  (* t is inductive, then CUMUL or CONV is irrelevant *)
 	  clenv_unify true CUMUL t (clenv_instance_type clause mv) clause in
-	elim_res_pf kONT clause' gl
+	elim_res_pf kONT clause' true gl
     | _ -> anomaly "elim_scheme_type"
 
 let elim_type t gl =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 29107c32a2..0c9744e2c6 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -158,7 +158,8 @@ val cut_and_apply         : constr -> tactic
 
 (*s Elimination tactics. *)
 
-val general_elim  : constr with_bindings -> constr with_bindings -> tactic
+val general_elim  : constr with_bindings -> constr with_bindings -> 
+  ?allow_K:bool -> tactic
 val default_elim  : constr with_bindings -> tactic
 val simplest_elim : constr -> tactic
 val elim          : constr with_bindings -> constr with_bindings option -> tactic
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index c3be3d98ab..46cadeb0af 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 *)