Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg

1 files changed, 50 insertions, 21 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cb98ec18..c863a453 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactics.ml 9605 2007-02-07 12:19:19Z notin $ *)
+(* $Id: tactics.ml 9853 2007-05-23 14:25:47Z letouzey $ *)
 
 open Pp
 open Util
@@ -503,6 +503,20 @@ let cut_in_parallel l =
   in 
     prec (List.rev l)
 
+let error_uninstantiated_metas t clenv =
+  let na = meta_name clenv.env (List.hd (Metaset.elements (metavars_of t))) in
+  let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta"
+  in errorlabstrm "" (str "cannot find an instance for " ++ pr_id id)
+
+let clenv_refine_in id clenv gl =
+  let new_hyp_typ  = clenv_type clenv in
+  if occur_meta new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv;
+  let new_hyp_prf  = clenv_value clenv in
+  tclTHEN
+    (tclEVARS (evars_of clenv.env))
+    (cut_replacing id new_hyp_typ
+      (fun x gl -> refine_no_check new_hyp_prf gl)) gl
+
 (****************************************************)
 (*            Resolution tactics                    *)
 (****************************************************)
@@ -575,12 +589,7 @@ let apply_in id lemmas gls =
   let t' = pf_get_hyp_typ gls id in
   let innermostclause = mk_clenv_from_n gls (Some 0) (mkVar id,t') in
   let clause = List.fold_left (apply_in_once gls) innermostclause lemmas in
-  let new_hyp_prf  = clenv_value clause in
-  let new_hyp_typ  = clenv_type clause in
-  tclTHEN
-    (tclEVARS (evars_of clause.env))
-    (cut_replacing id new_hyp_typ
-      (fun x gls -> refine_no_check new_hyp_prf gls)) gls
+  clenv_refine_in id clause gls
 
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
    |- B -> C and |- A
@@ -839,15 +848,11 @@ let elimination_in_clause_scheme id elimclause indclause gl =
   let hyp_typ = pf_type_of gl hyp in
   let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
   let elimclause'' = clenv_fchain hypmv elimclause' hypclause in  
-  let new_hyp_prf  = clenv_value elimclause'' in
   let new_hyp_typ  = clenv_type elimclause'' in
   if eq_constr hyp_typ new_hyp_typ then
     errorlabstrm "general_rewrite_in" 
       (str "Nothing to rewrite in " ++ pr_id id);
-  tclTHEN
-    (tclEVARS (evars_of elimclause''.env))
-    (cut_replacing id new_hyp_typ
-      (fun x gls -> refine_no_check new_hyp_prf gls)) gl
+  clenv_refine_in id elimclause'' gl
 
 let general_elim_in id =
   general_elim_clause (elimination_in_clause_scheme id)
@@ -2328,10 +2333,18 @@ let dImp cls =
 let setoid_reflexivity = ref (fun _ -> assert false)
 let register_setoid_reflexivity f = setoid_reflexivity := f
 
-let reflexivity gl =
-  match match_with_equation (pf_concl gl) with
+let reflexivity_red allowred gl =
+  (* PL: usual reflexivity don't perform any reduction when searching 
+     for an equality, but we may need to do some when called back from 
+     inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
+  let concl = if not allowred then pf_concl gl
+  else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) 
+  in 
+  match match_with_equation concl with
     | None -> !setoid_reflexivity gl
-    | Some (hdcncl,args) ->  one_constructor 1 NoBindings gl
+    | Some _ -> one_constructor 1 NoBindings gl
+
+let reflexivity gl = reflexivity_red false gl
 
 let intros_reflexivity  = (tclTHEN intros reflexivity)
 
@@ -2345,8 +2358,14 @@ let intros_reflexivity  = (tclTHEN intros reflexivity)
 let setoid_symmetry = ref (fun _ -> assert false)
 let register_setoid_symmetry f = setoid_symmetry := f
 
-let symmetry gl =
-  match match_with_equation (pf_concl gl) with
+let symmetry_red allowred gl =
+  (* PL: usual symmetry don't perform any reduction when searching 
+     for an equality, but we may need to do some when called back from 
+     inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
+  let concl = if not allowred then pf_concl gl
+  else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) 
+  in 
+  match match_with_equation concl with
     | None -> !setoid_symmetry gl
     | Some (hdcncl,args) ->
         let hdcncls = string_of_inductive hdcncl in
@@ -2360,7 +2379,7 @@ let symmetry gl =
               | [c1;c2]     -> mkApp (hdcncl, [| c2; c1 |])
 	      | _ -> assert false 
 	    in 
-	    tclTHENLAST (cut symc)
+	    tclTHENFIRST (cut symc)
               (tclTHENLIST 
 		[ intro;
 		  tclLAST_HYP simplest_case;
@@ -2368,6 +2387,8 @@ let symmetry gl =
 	      gl
 	end
 
+let symmetry gl = symmetry_red false gl
+
 let setoid_symmetry_in = ref (fun _ _ -> assert false)
 let register_setoid_symmetry_in f = setoid_symmetry_in := f
 
@@ -2408,8 +2429,14 @@ let intros_symmetry =
 let setoid_transitivity = ref (fun _ _ -> assert false)
 let register_setoid_transitivity f = setoid_transitivity := f
 
-let transitivity t gl =
-  match match_with_equation (pf_concl gl) with
+let transitivity_red allowred t gl =
+  (* PL: usual transitivity don't perform any reduction when searching 
+     for an equality, but we may need to do some when called back from 
+     inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
+  let concl = if not allowred then pf_concl gl
+  else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) 
+  in 
+  match match_with_equation concl with
     | None -> !setoid_transitivity t gl
     | Some (hdcncl,args) -> 
         let hdcncls = string_of_inductive hdcncl in
@@ -2436,7 +2463,9 @@ let transitivity t gl =
 		    tclLAST_HYP simplest_case;
 		    assumption ])) gl
         end 
-	
+
+let transitivity t gl = transitivity_red false t gl
+
 let intros_transitivity  n  = tclTHEN intros (transitivity n)
 
 (* tactical to save as name a subproof such that the generalisation of