Merge commit 'upstream/8.1.pl1+dfsg'

1 files changed, 44 insertions, 10 deletions

diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 8b2ce26b..f963fc9c 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(*i $Id: newring.ml4 9603 2007-02-07 00:41:16Z barras $ i*)
+(*i $Id: newring.ml4 9968 2007-07-11 15:49:07Z barras $ i*)
 
 open Pp
 open Util
@@ -166,8 +166,10 @@ let decl_constant na c =
       const_entry_boxed = true}, 
     IsProof Lemma))
 
-let ltac_call tac args =
+let ltac_call tac (args:glob_tactic_arg list) =
   TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args))
+let ltac_acall tac (args:glob_tactic_arg list) =
+  TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)
 
 let ltac_lcall tac args =
   TacArg(TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args))
@@ -276,12 +278,18 @@ let coq_mk_reqe = my_constant "mk_reqe"
 let coq_semi_ring_theory = my_constant "semi_ring_theory"
 let coq_mk_seqe = my_constant "mk_seqe"
 
+let ltac_inv_morph_gen = zltac"inv_gen_phi"
 let ltac_inv_morphZ = zltac"inv_gen_phiZ"
 let ltac_inv_morphN = zltac"inv_gen_phiN"
+let ltac_inv_morphNword = zltac"inv_gen_phiNword"
 let coq_abstract = my_constant"Abstract"
 let coq_comp = my_constant"Computational"
 let coq_morph = my_constant"Morphism"
 
+(* morphism *)
+let coq_ring_morph = my_constant "ring_morph"
+let coq_semi_morph = my_constant "semi_morph"
+
 (* power function *)
 let ltac_inv_morph_nothing = zltac"inv_morph_nothing"
 let coq_pow_N_pow_N = my_constant "pow_N_pow_N"
@@ -527,6 +535,18 @@ let dest_ring env sigma th_spec =
     | _ -> error "bad ring structure"
 
 
+let dest_morph env sigma m_spec =
+  let m_typ = Retyping.get_type_of env sigma m_spec in
+  match kind_of_term m_typ with
+      App(f,[|r;zero;one;add;mul;sub;opp;req;
+              c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|])
+        when f = Lazy.force coq_ring_morph ->
+          (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi)
+    | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|])
+        when f = Lazy.force coq_semi_morph ->
+        (c,czero,cone,cadd,cmul,None,None,ceqb,phi)
+    | _ -> error "bad morphism structure"
+
 
 type coeff_spec =
     Computational of constr (* equality test *)
@@ -545,22 +565,34 @@ type cst_tac_spec =
     CstTac of raw_tactic_expr
   | Closed of reference list
 
-let interp_cst_tac kind (zero,one,add,mul,opp) cst_tac =
+let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
   match cst_tac with
       Some (CstTac t) -> Tacinterp.glob_tactic t
     | Some (Closed lc) -> closed_term_ast (List.map Nametab.global lc)
     | None ->
-        (match opp, kind with
-            None, _ ->
+        (match rk, opp, kind with
+            Abstract, None, _ ->
               let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in
               TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul]))
-          | Some opp, Some _ ->
+          | Abstract, Some opp, Some _ ->
               let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in
               TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
-          | _ -> error"a tactic must be specified for an almost_ring")
+          | Abstract, Some opp, None ->
+              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in
+              TacArg
+                (TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
+          | Computational _,_,_ ->
+              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
+              TacArg
+                (TacCall(dummy_loc,t,List.map carg [zero;one;zero;one]))
+          | Morphism mth,_,_ ->
+              let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in
+              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
+              TacArg
+                (TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone])))
 
 let make_hyp env c =
-  let t = (Typeops.typing env c).uj_type in
+  let t = Retyping.get_type_of env Evd.empty c in
   lapp coq_mkhypo [|t;c|]
 
 let make_hyp_list env lH =
@@ -608,7 +640,8 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign =
 
   let lemma1 = decl_constant (string_of_id name^"_ring_lemma1") lemma1 in
   let lemma2 = decl_constant (string_of_id name^"_ring_lemma2") lemma2 in
-  let cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in
+  let cst_tac =
+    interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
     match pre with
         Some t -> Tacinterp.glob_tactic t
@@ -980,7 +1013,8 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign =
   let lemma3 = decl_constant (string_of_id name^"_field_lemma3") lemma3 in
   let lemma4 = decl_constant (string_of_id name^"_field_lemma4") lemma4 in
   let cond_lemma = decl_constant (string_of_id name^"_lemma5") cond_lemma in
-  let cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in
+  let cst_tac =
+    interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
     match pre with
         Some t -> Tacinterp.glob_tactic t