Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

5 files changed, 90 insertions, 90 deletions

diff --git a/contrib/field/Field.v b/contrib/field/Field.v
index 7b48e275..3cc097fc 100644
--- a/contrib/field/Field.v
+++ b/contrib/field/Field.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Field.v,v 1.6.2.1 2004/07/16 19:30:09 herbelin Exp $ *)
+(* $Id: Field.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Require Export Field_Compl.
 Require Export Field_Theory.
diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v
index cba921f7..774b3084 100644
--- a/contrib/field/Field_Compl.v
+++ b/contrib/field/Field_Compl.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Field_Compl.v,v 1.8.2.1 2004/07/16 19:30:09 herbelin Exp $ *)
+(* $Id: Field_Compl.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Inductive listT (A:Type) : Type :=
   | nilT : listT A
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index c5c06547..afa0a814 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Field_Tactic.v,v 1.20.2.1 2004/07/16 19:30:09 herbelin Exp $ *)
+(* $Id: Field_Tactic.v 8134 2006-03-05 16:39:17Z herbelin $ *)
 
 Require Import Ring.
 Require Export Field_Compl.
@@ -14,6 +14,10 @@ Require Export Field_Theory.
 
 (**** Interpretation A --> ExprA ****)
 
+Ltac get_component a s := eval cbv beta iota delta [a] in (a s).
+
+Ltac body_of s := eval cbv beta iota delta [s] in s.
+
 Ltac mem_assoc var lvar :=
   match constr:lvar with
   | (nilT _) => constr:false
@@ -24,49 +28,46 @@ Ltac mem_assoc var lvar :=
       end
   end.
 
-Ltac seek_var_aux FT lvar trm :=
-  let AT := eval cbv beta iota delta [A] in (A FT)
-  with AzeroT := eval cbv beta iota delta [Azero] in (Azero FT)
-  with AoneT := eval cbv beta iota delta [Aone] in (Aone FT)
-  with AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT)
-  with AmultT := eval cbv beta iota delta [Amult] in (Amult FT)
-  with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT)
-  with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in
-  match constr:trm with
-  | AzeroT => lvar
-  | AoneT => lvar
-  | (AplusT ?X1 ?X2) =>
-      let l1 := seek_var_aux FT lvar X1 in
-      seek_var_aux FT l1 X2
-  | (AmultT ?X1 ?X2) =>
-      let l1 := seek_var_aux FT lvar X1 in
-      seek_var_aux FT l1 X2
-  | (AoppT ?X1) => seek_var_aux FT lvar X1
-  | (AinvT ?X1) => seek_var_aux FT lvar X1
-  | ?X1 =>
-      let res := mem_assoc X1 lvar in
-      match constr:res with
-      | true => lvar
-      | false => constr:(consT AT X1 lvar)
-      end
-  end.
-
-Ltac seek_var FT trm :=
-  let AT := eval cbv beta iota delta [A] in (A FT) in
-  seek_var_aux FT (nilT AT) trm.
-
-Ltac number_aux lvar cpt :=
-  match constr:lvar with
-  | (nilT ?X1) => constr:(nilT (prodT X1 nat))
-  | (consT ?X1 ?X2 ?X3) =>
-      let l2 := number_aux X3 (S cpt) in
-      constr:(consT (prodT X1 nat) (pairT X1 nat X2 cpt) l2)
-  end.
-
-Ltac number lvar := number_aux lvar 0.
-
-Ltac build_varlist FT trm := let lvar := seek_var FT trm in
-                             number lvar.
+Ltac number lvar := 
+  let rec number_aux lvar cpt :=
+    match constr:lvar with
+    | (nilT ?X1) => constr:(nilT (prodT X1 nat))
+    | (consT ?X1 ?X2 ?X3) =>
+        let l2 := number_aux X3 (S cpt) in
+        constr:(consT (prodT X1 nat) (pairT X1 nat X2 cpt) l2) 
+    end
+  in number_aux lvar 0.
+
+Ltac build_varlist FT trm := 
+  let rec seek_var lvar trm :=
+    let AT := get_component A FT
+    with AzeroT := get_component Azero FT
+    with AoneT := get_component Aone FT
+    with AplusT := get_component Aplus FT
+    with AmultT := get_component Amult FT
+    with AoppT := get_component Aopp FT
+    with AinvT := get_component Ainv FT in
+    match constr:trm with
+    | AzeroT => lvar
+    | AoneT => lvar
+    | (AplusT ?X1 ?X2) =>
+        let l1 := seek_var lvar X1 in
+        seek_var l1 X2
+    | (AmultT ?X1 ?X2) =>
+        let l1 := seek_var lvar X1 in
+        seek_var l1 X2
+    | (AoppT ?X1) => seek_var lvar X1
+    | (AinvT ?X1) => seek_var lvar X1
+    | ?X1 =>
+        let res := mem_assoc X1 lvar in
+        match constr:res with
+        | true => lvar
+        | false => constr:(consT AT X1 lvar)
+        end
+    end in
+  let AT := get_component A FT in
+  let lvar := seek_var (nilT AT) trm in
+  number lvar.
 
 Ltac assoc elt lst :=
   match constr:lst with
@@ -79,13 +80,13 @@ Ltac assoc elt lst :=
   end.
 
 Ltac interp_A FT lvar trm :=
-  let AT := eval cbv beta iota delta [A] in (A FT)
-  with AzeroT := eval cbv beta iota delta [Azero] in (Azero FT)
-  with AoneT := eval cbv beta iota delta [Aone] in (Aone FT)
-  with AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT)
-  with AmultT := eval cbv beta iota delta [Amult] in (Amult FT)
-  with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT)
-  with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in
+  let AT := get_component A FT
+  with AzeroT := get_component Azero FT
+  with AoneT := get_component Aone FT
+  with AplusT := get_component Aplus FT
+  with AmultT := get_component Amult FT
+  with AoppT := get_component Aopp FT
+  with AinvT := get_component Ainv FT in
   match constr:trm with
   | AzeroT => constr:EAzero
   | AoneT => constr:EAone
@@ -181,18 +182,17 @@ Ltac weak_reduce :=
 
 Ltac multiply mul :=
   match goal with
-  |  |- (interp_ExprA ?X1 ?X2 ?X3 = interp_ExprA ?X1 ?X2 ?X4) =>
-      let AzeroT := eval cbv beta iota delta [Azero X1] in (Azero X1) in
-      (cut (interp_ExprA X1 X2 mul <> AzeroT);
-        [ intro; let id := grep_mult in
-                 apply (mult_eq X1 X3 X4 mul X2 id)
+  |  |- (interp_ExprA ?FT ?X2 ?X3 = interp_ExprA ?FT ?X2 ?X4) =>
+      let AzeroT := get_component Azero FT in
+      (cut (interp_ExprA FT X2 mul <> AzeroT);
+        [ intro; let id := grep_mult in apply (mult_eq FT X3 X4 mul X2 id)
         | weak_reduce;
-           let AoneT := eval cbv beta iota delta [Aone X1] in (Aone X1)
-           with AmultT := eval cbv beta iota delta [Amult X1] in (Amult X1) in
+           let AoneT := get_component Aone ltac:(body_of FT)
+           with AmultT := get_component Amult ltac:(body_of FT) in
            (try
              match goal with
-             |  |- context [(AmultT _ AoneT)] => rewrite (AmultT_1r X1)
-             end; clear X1 X2) ])
+             |  |- context [(AmultT _ AoneT)] => rewrite (AmultT_1r FT)
+             end; clear FT X2) ])
   end.
 
 Ltac apply_multiply FT lvar trm :=
@@ -219,10 +219,10 @@ Ltac apply_inverse mul FT lvar trm :=
 Ltac strong_fail tac := first [ tac | fail 2 ].
 
 Ltac inverse_test_aux FT trm :=
-  let AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT)
-  with AmultT := eval cbv beta iota delta [Amult] in (Amult FT)
-  with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT)
-  with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in
+  let AplusT := get_component Aplus FT
+  with AmultT := get_component Amult FT
+  with AoppT := get_component Aopp FT
+  with AinvT := get_component Ainv FT in
   match constr:trm with
   | (AinvT _) => fail 1
   | (AoppT ?X1) =>
@@ -235,7 +235,7 @@ Ltac inverse_test_aux FT trm :=
   end.
 
 Ltac inverse_test FT :=
-  let AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT) in
+  let AplusT := get_component Aplus FT in
   match goal with
   |  |- (?X1 = ?X2) => inverse_test_aux FT (AplusT X1 X2)
   end.
@@ -253,27 +253,27 @@ Ltac apply_simplif sfun :=
    end.
 
 Ltac unfolds FT :=
-  match eval cbv beta iota delta [Aminus] in (Aminus FT) with
+  match get_component Aminus FT with
   | (Field_Some _ ?X1) => unfold X1 in |- *
   | _ => idtac
   end;
-   match eval cbv beta iota delta [Adiv] in (Adiv FT) with
+   match get_component Adiv FT with
    | (Field_Some _ ?X1) => unfold X1 in |- *
    | _ => idtac
    end.
 
 Ltac reduce FT :=
-  let AzeroT := eval cbv beta iota delta [Azero] in (Azero FT)
-  with AoneT := eval cbv beta iota delta [Aone] in (Aone FT)
-  with AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT)
-  with AmultT := eval cbv beta iota delta [Amult] in (Amult FT)
-  with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT)
-  with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in
+  let AzeroT := get_component Azero FT
+  with AoneT := get_component Aone FT
+  with AplusT := get_component Aplus FT
+  with AmultT := get_component Amult FT
+  with AoppT := get_component Aopp FT
+  with AinvT := get_component Ainv FT in
   (cbv beta iota zeta delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] in |- * ||
      compute in |- *).
 
 Ltac field_gen_aux FT :=
-  let AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT) in
+  let AplusT := get_component Aplus FT in
   match goal with
   |  |- (?X1 = ?X2) =>
       let lvar := build_varlist FT (AplusT X1 X2) in
@@ -303,11 +303,11 @@ Ltac field_gen FT := unfolds FT; (inverse_test FT; ring) || field_gen_aux FT.
 
 Ltac init_exp FT trm :=
   let e :=
-   (match eval cbv beta iota delta [Aminus] in (Aminus FT) with
+   (match get_component Aminus FT with
     | (Field_Some _ ?X1) => eval cbv beta delta [X1] in trm
     | _ => trm
     end) in
-  match eval cbv beta iota delta [Adiv] in (Adiv FT) with
+  match get_component Adiv FT with
   | (Field_Some _ ?X1) => eval cbv beta delta [X1] in e
   | _ => e
   end.
@@ -429,4 +429,4 @@ Ltac field_term FT exp :=
    simpl_all_monomials
     ltac:(assoc_distrib ltac:(simpl_all_monomials ltac:(simpl_inv tma))) in
   let trep := eval_weak_reduce (interp_ExprA FT lvar tsmp) in
-  (replace exp with trep; [ ring trep | field_gen FT ]).
\ No newline at end of file
+  (replace exp with trep; [ ring trep | field_gen FT ]).
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
index 8737fd79..2c954652 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/Field_Theory.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Field_Theory.v,v 1.12.2.1 2004/07/16 19:30:09 herbelin Exp $ *)
+(* $Id: Field_Theory.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Require Import Peano_dec.
 Require Import Ring.
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 32adec66..35591f23 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: field.ml4,v 1.33.2.1 2004/07/16 19:30:09 herbelin Exp $ *)
+(* $Id: field.ml4 7837 2006-01-11 09:47:32Z herbelin $ *)
 
 open Names
 open Pp
@@ -21,6 +21,7 @@ open Util
 open Vernacinterp
 open Vernacexpr
 open Tacexpr
+open Mod_subst
 
 (* Interpretation of constr's *)
 let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
@@ -43,7 +44,7 @@ let lookup env typ =
   with Not_found -> 
     errorlabstrm "field"
       (str "No field is declared for type" ++ spc() ++
-      Printer.prterm_env env typ)
+      Printer.pr_lconstr_env env typ)
 
 let _ = 
   let init () = th_tab := Gmap.empty in
@@ -113,8 +114,8 @@ END
 *)
 
 (* For the translator, otherwise the code above is OK *)
-open Ppconstrnew
-let pp_minus_div_arg _prc _prt (omin,odiv) = 
+open Ppconstr
+let pp_minus_div_arg _prc _prlc _prt (omin,odiv) = 
   if omin=None && odiv=None then mt() else
     spc() ++ str "with" ++
     pr_opt (fun c -> str "minus := " ++ _prc c) omin ++
@@ -149,8 +150,7 @@ END
 
 (* Guesses the type and calls field_gen with the right theory *)
 let field g =
-  Library.check_required_library ["Coq";"field";"Field"];
-  let ist = { lfun=[]; debug=get_debug () } in
+  Coqlib.check_required_library ["Coq";"field";"Field"];
   let typ = 
     match Hipattern.match_with_equation (pf_concl g) with
       | Some (eq,t::args) when eq = (Coqlib.build_coq_eq_data()).Coqlib.eq -> t
@@ -172,7 +172,7 @@ let guess_theory env evc = function
 
 (* Guesses the type and calls Field_Term with the right theory *)
 let field_term l g =
-  Library.check_required_library ["Coq";"field";"Field"];
+  Coqlib.check_required_library ["Coq";"field";"Field"];
   let env = (pf_env g)
   and evc = (project g) in
   let th = valueIn (VConstr (guess_theory env evc l))
@@ -184,7 +184,7 @@ let field_term l g =
 
 (* Declaration of Field *)
 
-TACTIC EXTEND Field
-| [ "Field" ] -> [ field ]
-| [ "Field" ne_constr_list(l) ] -> [ field_term l ]
+TACTIC EXTEND field
+| [ "field" ] -> [ field ]
+| [ "field" ne_constr_list(l) ] -> [ field_term l ]
 END