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

2 files changed, 90 insertions, 59 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index c14462eb..9c23dda5 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: setoid_replace.ml 9853 2007-05-23 14:25:47Z letouzey $ *)
+(* $Id: setoid_replace.ml 10213 2007-10-10 13:05:59Z letouzey $ *)
 
 open Tacmach
 open Proof_type
@@ -819,15 +819,16 @@ let new_morphism m signature id hook =
 	    try find_relation_class output' 
 	    with Not_found -> errorlabstrm "Add Morphism"
 	      (str "Not a valid signature: " ++ pr_lconstr output' ++
-		  str " is neither a registered relation nor the Leibniz " ++
-		  str " equality.") in
+		 str " is neither a registered relation nor the Leibniz " ++
+		 str " equality.") in
 	  let rel_a,rel_quantifiers_no =
             match rel with
 		Relation rel -> rel.rel_a, rel.rel_quantifiers_no
               | Leibniz (Some t) -> t, 0
-              | Leibniz None -> assert false in
+              | Leibniz None -> let _,t = decompose_prod typ in t, 0 in
 	  let rel_a_n =
-            clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a in
+            clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a 
+	  in
 	    try
               let _,output_rel_a_n = decompose_lam_n rel_quantifiers_no rel_a_n in
               let argsrev,_ = decompose_prod output_rel_a_n in
@@ -1890,47 +1891,49 @@ let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_
       | Some tac ->  Tacticals.tclTRY (Tacticals.tclCOMPLETE tac )
   in 
   try
-  let relation =
-   match relation with
-      Some rel ->
-       (try
-         match find_relation_class rel with
-            Relation sa -> sa
-          | Leibniz _ -> raise Optimize
-        with
-         Not_found ->
-          errorlabstrm "Setoid_rewrite"
-           (pr_lconstr rel ++ str " is not a registered relation."))
-    | None ->
-       match default_relation_for_carrier (pf_type_of gl c1) with
-          Relation sa -> sa
-        | Leibniz _ -> raise Optimize
-  in
-   let eq_left_to_right = mkApp (relation.rel_aeq, [| c1 ; c2 |]) in
-   let eq_right_to_left = mkApp (relation.rel_aeq, [| c2 ; c1 |]) in
-   let replace dir eq =
-    tclTHENS (assert_tac false Anonymous eq)
-      [onLastHyp (fun id ->
-        tclTHEN
-          (rewrite_tac dir (mkVar id) ~new_goals)
-          (clear [id]));
-       try_prove_eq_tac]
-   in
-    tclORELSE
-     (replace true eq_left_to_right) (replace false eq_right_to_left) gl
- with
-  Optimize -> (* (!replace tac_opt c1 c2) gl *)
-    let eq =  mkApp (Lazy.force  coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in 
-    tclTHENS (assert_tac false Anonymous eq)
-      [onLastHyp (fun id ->
-		    tclTHEN
-		      (rewrite_tac false (mkVar id) ~new_goals)
-		      (clear [id]));
-       try_prove_eq_tac] gl
+    let carrier,args = decompose_app (pf_type_of gl c1) in
+    let relation =
+      match relation with
+	  Some rel ->
+	    (try
+		match find_relation_class rel with
+		    Relation sa -> if not (eq_constr carrier sa.rel_a) then 		    
+			errorlabstrm "Setoid_rewrite"
+			  (str "the carrier of " ++ pr_lconstr rel ++ 
+			      str " does not match the type of " ++ pr_lconstr c1);
+		      sa
+		  | Leibniz _ -> raise Optimize
+              with
+		  Not_found ->
+		    errorlabstrm "Setoid_rewrite"
+		      (pr_lconstr rel ++ str " is not a registered relation."))
+	| None ->
+	    match default_relation_for_carrier (pf_type_of gl c1) with
+		Relation sa -> sa
+              | Leibniz _ -> raise Optimize
+    in
+    let eq_left_to_right = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c1 ; c2 ])) in
+    let eq_right_to_left = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c2 ; c1 ])) in
+    let replace dir eq =
+      tclTHENS (assert_tac false Anonymous eq)
+	[onLastHyp (fun id ->
+          tclTHEN
+            (rewrite_tac dir (mkVar id) ~new_goals)
+            (clear [id]));
+	 try_prove_eq_tac]
+    in
+      tclORELSE
+	(replace true eq_left_to_right) (replace false eq_right_to_left) gl
+  with
+      Optimize -> (* (!replace tac_opt c1 c2) gl *)
+	let eq =  mkApp (Lazy.force  coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in 
+	  tclTHENS (assert_tac false Anonymous eq)
+	    [onLastHyp (fun id ->
+	      tclTHEN
+		(rewrite_tac false (mkVar id) ~new_goals)
+		(clear [id]));
+	     try_prove_eq_tac] gl
       
-
-
-
 let setoid_replace = general_setoid_replace general_s_rewrite
 let setoid_replace_in  tac_opt id relation c1 c2 ~new_goals gl = 
   general_setoid_replace (general_s_rewrite_in id)  tac_opt relation c1 c2 ~new_goals gl
@@ -1970,11 +1973,22 @@ let setoid_symmetry gl =
   Optimize -> symmetry_red true gl
 
 let setoid_symmetry_in id gl =
- let new_hyp =
-  let _,he,c1,c2 = analyse_hypothesis gl (mkVar id) in
-   mkApp (he, [| c2 ; c1 |])
- in
- cut_replacing id new_hyp (tclTHEN setoid_symmetry) gl
+  let ctype = pf_type_of gl (mkVar id) in
+  let binders,concl = Sign.decompose_prod_assum ctype in
+  let (equiv, args) = decompose_app concl in
+  let rec split_last_two = function
+    | [c1;c2] -> [],(c1, c2)
+    | x::y::z -> let l,res = split_last_two (y::z) in x::l, res
+    | _ -> error "The term provided is not an equivalence" 
+  in
+  let others,(c1,c2) = split_last_two args in
+  let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
+  let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
+  let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
+  tclTHENS (cut new_hyp)
+    [ intro_replacing id;
+      tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); assumption ] ]
+    gl
 
 let setoid_transitivity c gl =
  try
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ac6a396f..37b3cbcb 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacinterp.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: tacinterp.ml 10135 2007-09-21 14:28:12Z herbelin $ *)
 
 open Constrintern
 open Closure
@@ -436,9 +436,16 @@ let rec intern_intro_pattern lf ist = function
 and intern_case_intro_pattern lf ist =
   List.map (List.map (intern_intro_pattern lf ist))
 
-let intern_quantified_hypothesis ist x =
-  (* We use identifier both for variables and quantified hyps (no way to
-     statically check the existence of a quantified hyp); thus nothing to do *)
+let intern_quantified_hypothesis ist = function
+  | AnonHyp n -> AnonHyp n
+  | NamedHyp id ->
+      (* Uncomment to disallow "intros until n" in ltac when n is not bound *)
+      NamedHyp ((*snd (intern_hyp ist (dloc,*)id(* ))*))
+      
+let intern_binding_name ist x =
+  (* We use identifier both for variables and binding names *)
+  (* Todo: consider the body of the lemma to which the binding refer 
+     and if a term w/o ltac vars, check the name is indeed quantified *)
   x
 
 let intern_constr_gen isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
@@ -453,7 +460,7 @@ let intern_type = intern_constr_gen true
 
 (* Globalize bindings *)
 let intern_binding ist (loc,b,c) =
-  (loc,intern_quantified_hypothesis ist b,intern_constr ist c)
+  (loc,intern_binding_name ist b,intern_constr ist c)
 
 let intern_bindings ist = function
   | NoBindings -> NoBindings
@@ -1465,8 +1472,17 @@ let interp_quantified_hypothesis ist = function
   | AnonHyp n -> AnonHyp n
   | NamedHyp id ->
       try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
-      with Not_found 
-      | Stdpp.Exc_located (_, UserError _) | UserError _ (*Compat provisoire*)
+      with Not_found | Stdpp.Exc_located (_, UserError _) | UserError _
+   -> NamedHyp id
+
+let interp_binding_name ist = function
+  | AnonHyp n -> AnonHyp n
+  | NamedHyp id ->
+      (* If a name is bound, it has to be a quantified hypothesis *)
+      (* user has to use other names for variables if these ones clash with *)
+      (* a name intented to be used as a (non-variable) identifier *)
+      try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
+      with Not_found | Stdpp.Exc_located (_, UserError _) | UserError _ 
    -> NamedHyp id
 
 (* Quantified named or numbered hypothesis or hypothesis in context *)
@@ -1495,7 +1511,7 @@ let interp_induction_arg ist gl = function
 	(pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))))
 
 let interp_binding ist gl (loc,b,c) =
-  (loc,interp_quantified_hypothesis ist b,pf_interp_constr ist gl c)
+  (loc,interp_binding_name ist b,pf_interp_constr ist gl c)
 
 let interp_bindings ist gl = function
 | NoBindings -> NoBindings
@@ -2349,7 +2365,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacMutualCofix (id,l) ->
       TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
   | TacCut c -> TacCut (subst_rawconstr subst c)
-  | TacAssert (b,na,c) -> TacAssert (b,na,subst_rawconstr subst c)
+  | TacAssert (b,na,c) ->
+      TacAssert (option_map (subst_tactic subst) b,na,subst_rawconstr subst c)
   | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl)
   | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c)
   | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp)