Imported Upstream version 8.3pl1upstream/8.3pl1

4 files changed, 74 insertions, 23 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6b16adb4..7a774cc9 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: equality.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: equality.ml 13586 2010-10-27 17:42:13Z jforest $ *)
 
 open Pp
 open Util
@@ -185,12 +185,30 @@ let find_elim hdcncl lft2rgt dep cls args gl =
       pf_conv_x gl (List.nth args 0) (List.nth args 2)) && not dep
     || Flags.version_less_or_equal Flags.V8_2
   then
-    (* use eq_rect, eq_rect_r, JMeq_rect, etc for compatibility *)
-    let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
-    let hdcncls = string_of_inductive hdcncl ^ suffix in
-    let rwr_thm = if lft2rgt = Some (cls=None) then hdcncls^"_r" else hdcncls in
-    try pf_global gl (id_of_string rwr_thm)
-    with Not_found -> error ("Cannot find rewrite principle "^rwr_thm^".")
+    match kind_of_term hdcncl with 
+      | Ind ind_sp -> 
+	let pr1 = 
+	  lookup_eliminator ind_sp (elimination_sort_of_clause cls gl) 
+	in 
+	if lft2rgt = Some (cls=None) 
+	then
+	  let c1 = destConst pr1 in 
+	  let mp,dp,l = repr_con (constant_of_kn (canonical_con c1)) in 
+	  let l' = label_of_id (add_suffix (id_of_label l) "_r")  in 
+	  let c1' = Global.constant_of_delta (make_con mp dp l') in
+	  begin 
+	    try 
+	      let _ = Global.lookup_constant c1' in
+	      mkConst c1'
+	    with Not_found -> 
+	      let rwr_thm = string_of_label l' in 
+	      error ("Cannot find rewrite principle "^rwr_thm^".")
+	  end
+	else pr1 
+      | _ -> 
+	  (* cannot occur since we checked that we are in presence of 
+	     Logic.eq or Jmeq just before *)
+	assert false
   else
   let scheme_name = match dep, lft2rgt, inccl with
     (* Non dependent case with symmetric equality *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 3f069ab2..dfc8b6bf 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: extratactics.ml4 13434 2010-09-18 20:11:37Z msozeau $ *)
+(* $Id: extratactics.ml4 13658 2010-11-29 11:09:05Z glondu $ *)
 
 open Pp
 open Pcoq
@@ -545,7 +545,7 @@ let subst_var_with_hole occ tid t =
     | RVar (_,id) as x -> 
         if id = tid 
         then (decr occref; if !occref = 0 then x
-                           else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true))))
+                           else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))))
         else x
     | c -> map_rawconstr_left_to_right substrec c in
   let t' = substrec t
@@ -558,7 +558,7 @@ let subst_hole_with_term occ tc t =
   let rec substrec = function
     | RHole (_,Evd.QuestionMark(Evd.Define true)) -> 
         decr occref; if !occref = 0 then tc
-                     else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true)))
+                     else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))
     | c -> map_rawconstr_left_to_right substrec c
   in
   substrec t
@@ -580,8 +580,8 @@ let hResolve id c occ t gl =
     try 
       Pretyping.Default.understand sigma env t_hole
     with 
-    | Ploc.Exc (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> 
-        resolve_hole (subst_hole_with_term (Ploc.line_nb loc) c_raw t_hole)
+    | Stdpp.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> 
+        resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole)
   in
   let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
   let t_constr_type = Retyping.get_type_of env sigma t_constr in
@@ -629,3 +629,36 @@ TACTIC EXTEND constr_eq
 | [ "constr_eq" constr(x) constr(y) ] -> [ 
     if eq_constr x y then tclIDTAC else tclFAIL 0 (str "Not equal") ]
 END
+
+TACTIC EXTEND is_evar
+| [ "is_evar" constr(x) ] ->
+    [ match kind_of_term x with
+        | Evar _ -> tclIDTAC
+        | _ -> tclFAIL 0 (str "Not an evar")
+    ]
+END
+
+let rec has_evar x =
+  match kind_of_term x with
+    | Evar _ -> true
+    | Rel _ | Var _ | Meta _ | Sort _ | Const _ | Ind _ | Construct _ ->
+      false
+    | Cast (t1, _, t2) | Prod (_, t1, t2) | Lambda (_, t1, t2) ->
+      has_evar t1 || has_evar t2
+    | LetIn (_, t1, t2, t3) ->
+      has_evar t1 || has_evar t2 || has_evar t3
+    | App (t1, ts) ->
+      has_evar t1 || has_evar_array ts
+    | Case (_, t1, t2, ts) ->
+      has_evar t1 || has_evar t2 || has_evar_array ts
+    | Fix ((_, tr)) | CoFix ((_, tr)) ->
+      has_evar_prec tr
+and has_evar_array x =
+  array_exists has_evar x
+and has_evar_prec (_, ts1, ts2) =
+  array_exists has_evar ts1 || array_exists has_evar ts2
+
+TACTIC EXTEND has_evar
+| [ "has_evar" constr(x) ] ->
+    [ if has_evar x then tclIDTAC else tclFAIL 0 (str "No evars") ]
+END
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index d8497a7d..360be9ef 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -596,13 +596,13 @@ let make_leibniz_proof c ty r =
 	let prf =
 	  mkApp (Lazy.force coq_f_equal,
 		[| r.rew_car; ty;
-		   mkLambda (Anonymous, r.rew_car, c (mkRel 1));
+		   mkLambda (Anonymous, r.rew_car, c);
 		   r.rew_from; r.rew_to; prf |])
 	in RewPrf (rel, prf)
     | RewCast k -> r.rew_prf
   in
     { r with rew_car = ty; 
-      rew_from = c r.rew_from; rew_to = c r.rew_to; rew_prf = prf }
+      rew_from = subst1 r.rew_from c; rew_to = subst1 r.rew_to c; rew_prf = prf }
 
 open Elimschemes
 
@@ -772,21 +772,21 @@ let subterm all flags (s : strategy) : strategy =
 	  let c' = s env sigma c cty cstr' evars in
 	    (match c' with
 	    | Some (Some r) ->
-		Some (Some (make_leibniz_proof (fun x -> mkCase (ci, p, x, brs)) ty r))
+		Some (Some (make_leibniz_proof (mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs)) ty r))
 	    | x ->
 		if array_for_all ((=) 0) ci.ci_cstr_nargs then
 		  let cstr = Some (mkApp (Lazy.force coq_eq, [| ty |])) in
 		  let found, brs' = Array.fold_left (fun (found, acc) br ->
-		    if found <> None then (found, fun x -> br :: acc x)
+		    if found <> None then (found, fun x -> lift 1 br :: acc x)
 		    else
 		      match s env sigma br ty cstr evars with
-		      | Some (Some r) -> (Some r, fun x -> x :: acc x)
-		      | _ -> (None, fun x -> br :: acc x))
+		      | Some (Some r) -> (Some r, fun x -> mkRel 1 :: acc x)
+		      | _ -> (None, fun x -> lift 1 br :: acc x))
 		    (None, fun x -> []) brs
 		  in
 		    match found with
 		    | Some r ->
-			let ctxc x = mkCase (ci, p, c, Array.of_list (List.rev (brs' x))) in
+			let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' x))) in
 			  Some (Some (make_leibniz_proof ctxc ty r))
 		    | None -> x
 		else
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4ecc4739..569cf356 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactics.ml 13464 2010-09-24 22:23:02Z herbelin $ *)
+(* $Id: tactics.ml 13693 2010-12-08 15:32:25Z msozeau $ *)
 
 open Pp
 open Util
@@ -2365,8 +2365,8 @@ let abstract_args gl generalize_vars dep id defined f args =
   in 
   let f', args' = decompose_indapp f args in
   let parvars = ids_of_constr ~all:true Idset.empty f' in
+  let seen = ref parvars in
   let dogen, f', args' =
-    let seen = ref parvars in
     let find i x = not (isVar x) || 
       let v = destVar x in
 	if is_defined_variable env v || Idset.mem v !seen then true
@@ -2379,8 +2379,8 @@ let abstract_args gl generalize_vars dep id defined f args =
 	    true, mkApp (f', before), after
   in
     if dogen then
-      let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = 
-	Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],parvars,Idset.empty,env) args'
+      let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env =
+	Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],!seen,Idset.empty,env) args'
       in
       let args, refls = List.rev args, List.rev refls in
       let vars =