Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg

7 files changed, 138 insertions, 139 deletions

diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
index fd134899..956ece79 100644
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ b/plugins/extraction/ExtrOcamlNatInt.v
@@ -14,6 +14,10 @@ Require Import ExtrOcamlBasic.
 (** Disclaimer: trying to obtain efficient certified programs
     by extracting [nat] into [int] is definitively *not* a good idea:
 
+    - This is just a syntactic adaptation, many things can go wrong,
+    such as name captures (e.g. if you have a constant named "int"
+    in your development, or a module named "Pervasives"). See bug #2878.
+
     - Since [int] is bounded while [nat] is (theoretically) infinite,
     you have to make sure by yourself that your program will not
     manipulate numbers greater than [max_int]. Otherwise you should
@@ -34,17 +38,17 @@ Require Import ExtrOcamlBasic.
 (** Mapping of [nat] into [int]. The last string corresponds to
     a [nat_case], see documentation of [Extract Inductive]. *)
 
-Extract Inductive nat => int [ "0" "succ" ]
+Extract Inductive nat => int [ "0" "Pervasives.succ" ]
  "(fun fO fS n -> if n=0 then fO () else fS (n-1))".
 
 (** Efficient (but uncertified) versions for usual [nat] functions *)
 
 Extract Constant plus => "(+)".
-Extract Constant pred => "fun n -> max 0 (n-1)".
-Extract Constant minus => "fun n m -> max 0 (n-m)".
+Extract Constant pred => "fun n -> Pervasives.max 0 (n-1)".
+Extract Constant minus => "fun n m -> Pervasives.max 0 (n-m)".
 Extract Constant mult => "( * )".
-Extract Inlined Constant max => max.
-Extract Inlined Constant min => min.
+Extract Inlined Constant max => "Pervasives.max".
+Extract Inlined Constant min => "Pervasives.min".
 (*Extract Inlined Constant nat_beq => "(=)".*)
 Extract Inlined Constant EqNat.beq_nat => "(=)".
 Extract Inlined Constant EqNat.eq_nat_decide => "(=)".
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
index c8c40e73..ab634329 100644
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ b/plugins/extraction/ExtrOcamlZInt.v
@@ -34,12 +34,12 @@ Extract Inductive N => int [ "0" "" ]
 (** Efficient (but uncertified) versions for usual functions *)
 
 Extract Constant Pos.add => "(+)".
-Extract Constant Pos.succ => "succ".
-Extract Constant Pos.pred => "fun n -> max 1 (n-1)".
-Extract Constant Pos.sub => "fun n m -> max 1 (n-m)".
+Extract Constant Pos.succ => "Pervasives.succ".
+Extract Constant Pos.pred => "fun n -> Pervasives.max 1 (n-1)".
+Extract Constant Pos.sub => "fun n m -> Pervasives.max 1 (n-m)".
 Extract Constant Pos.mul => "( * )".
-Extract Constant Pos.min => "min".
-Extract Constant Pos.max => "max".
+Extract Constant Pos.min => "Pervasives.min".
+Extract Constant Pos.max => "Pervasives.max".
 Extract Constant Pos.compare =>
  "fun x y -> if x=y then Eq else if x<y then Lt else Gt".
 Extract Constant Pos.compare_cont =>
@@ -47,12 +47,12 @@ Extract Constant Pos.compare_cont =>
 
 
 Extract Constant N.add => "(+)".
-Extract Constant N.succ => "succ".
-Extract Constant N.pred => "fun n -> max 0 (n-1)".
-Extract Constant N.sub => "fun n m -> max 0 (n-m)".
+Extract Constant N.succ => "Pervasives.succ".
+Extract Constant N.pred => "fun n -> Pervasives.max 0 (n-1)".
+Extract Constant N.sub => "fun n m -> Pervasives.max 0 (n-m)".
 Extract Constant N.mul => "( * )".
-Extract Constant N.min => "min".
-Extract Constant N.max => "max".
+Extract Constant N.min => "Pervasives.min".
+Extract Constant N.max => "Pervasives.max".
 Extract Constant N.div => "fun a b -> if b=0 then 0 else a/b".
 Extract Constant N.modulo => "fun a b -> if b=0 then a else a mod b".
 Extract Constant N.compare =>
@@ -60,19 +60,19 @@ Extract Constant N.compare =>
 
 
 Extract Constant Z.add => "(+)".
-Extract Constant Z.succ => "succ".
-Extract Constant Z.pred => "pred".
+Extract Constant Z.succ => "Pervasives.succ".
+Extract Constant Z.pred => "Pervasives.pred".
 Extract Constant Z.sub => "(-)".
 Extract Constant Z.mul => "( * )".
 Extract Constant Z.opp => "(~-)".
-Extract Constant Z.abs => "abs".
-Extract Constant Z.min => "min".
-Extract Constant Z.max => "max".
+Extract Constant Z.abs => "Pervasives.abs".
+Extract Constant Z.min => "Pervasives.min".
+Extract Constant Z.max => "Pervasives.max".
 Extract Constant Z.compare =>
  "fun x y -> if x=y then Eq else if x<y then Lt else Gt".
 
 Extract Constant Z.of_N => "fun p -> p".
-Extract Constant Z.abs_N => "abs".
+Extract Constant Z.abs_N => "Pervasives.abs".
 
 (** Z.div and Z.modulo are quite complex to define in terms of (/) and (mod).
     For the moment we don't even try *)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index e76c6919..0a17453c 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -130,7 +130,7 @@ let rec nb_default_params env c =
 
 (* Enriching a signature with implicit information *)
 
-let sign_with_implicits r s =
+let sign_with_implicits r s nb_params =
   let implicits = implicits_of_global r in
   let rec add_impl i = function
     | [] -> []
@@ -139,7 +139,7 @@ let sign_with_implicits r s =
 	  if sign = Keep && List.mem i implicits then Kill Kother else sign
 	in sign' :: add_impl (succ i) s
   in
-  add_impl 1 s
+  add_impl (1+nb_params) s
 
 (* Enriching a exception message *)
 
@@ -667,20 +667,23 @@ and extract_cst_app env mle mlt kn args =
   let head = put_magic_if magic1 (MLglob (ConstRef kn)) in
   (* Now, the extraction of the arguments. *)
   let s_full = type2signature env (snd schema) in
-  let s_full = sign_with_implicits (ConstRef kn) s_full in
+  let s_full = sign_with_implicits (ConstRef kn) s_full 0 in
   let s = sign_no_final_keeps s_full in
   let ls = List.length s in
   let la = List.length args in
   (* The ml arguments, already expunged from known logical ones *)
   let mla = make_mlargs env mle s args metas in
   let mla =
-    if not magic1 then
+    if magic1 || lang () <> Ocaml then mla
+    else
       try
+        (* for better optimisations later, we discard dependent args
+           of projections and replace them by fake args that will be
+           removed during final pretty-print. *)
 	let l,l' = list_chop (projection_arity (ConstRef kn)) mla in
 	if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
 	else mla
       with _ -> mla
-    else mla
   in
   (* For strict languages, purely logical signatures with at least
      one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
@@ -726,7 +729,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let type_cons = instantiation (nb_tvars, type_cons) in
   (* Then, the usual variables [s], [ls], [la], ... *)
   let s = List.map (type2sign env) types in
-  let s = sign_with_implicits (ConstructRef cp) s in
+  let s = sign_with_implicits (ConstructRef cp) s params_nb in
   let ls = List.length s in
   let la = List.length args in
   assert (la <= ls + params_nb);
@@ -805,7 +808,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	let l = List.map f oi.ip_types.(i) in
 	(* the corresponding signature *)
 	let s = List.map (type2sign env) oi.ip_types.(i) in
-	let s = sign_with_implicits r s in
+	let s = sign_with_implicits r s mi.ind_nparams in
 	(* Extraction of the branch (in functional form). *)
 	let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in
 	(* We suppress dummy arguments according to signature. *)
@@ -876,7 +879,7 @@ let extract_std_constant env kn body typ =
   let l,t' = type_decomp (expand env (var2var' t)) in
   let s = List.map (type2sign env) l in
   (* Check for user-declared implicit information *)
-  let s = sign_with_implicits (ConstRef kn) s in
+  let s = sign_with_implicits (ConstRef kn) s 0 in
   (* Decomposing the top level lambdas of [body].
      If there isn't enough, it's ok, as long as remaining args
      aren't to be pruned (and initial lambdas aren't to be all
@@ -923,6 +926,19 @@ let extract_std_constant env kn body typ =
   in
   trm, type_expunge_from_sign env s t
 
+(* Extracts the type of an axiom, honors the Extraction Implicit declaration. *)
+let extract_axiom env kn typ =
+  reset_meta_count ();
+  (* The short type [t] (i.e. possibly with abbreviations). *)
+  let t = snd (record_constant_type env kn (Some typ)) in
+  (* The real type [t']: without head products, expanded, *)
+  (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
+  let l,_ = type_decomp (expand env (var2var' t)) in
+  let s = List.map (type2sign env) l in
+  (* Check for user-declared implicit information *)
+  let s = sign_with_implicits (ConstRef kn) s 0 in
+  type_expunge_from_sign env s t
+
 let extract_fixpoint env vkn (fi,ti,ci) =
   let n = Array.length vkn in
   let types = Array.make n (Tdummy Kother)
@@ -959,8 +975,8 @@ let extract_constant env kn cb =
     in Dtype (r, vl, t)
   in
   let mk_ax () =
-    let t = snd (record_constant_type env kn (Some typ)) in
-    Dterm (r, MLaxiom, type_expunge env t)
+    let t = extract_axiom env kn typ in
+    Dterm (r, MLaxiom, t)
   in
   let mk_def c =
     let e,t = extract_std_constant env kn c typ in
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 257e1c1c..bd997d2d 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -26,9 +26,9 @@ let rec msid_of_mt = function
 (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
    [ml_structure]. *)
 
-let se_iter do_decl do_spec =
+let se_iter do_decl do_spec do_mp =
   let rec mt_iter = function
-    | MTident _ -> ()
+    | MTident mp -> do_mp mp
     | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
     | MTwith (mt,ML_With_type(idl,l,t))->
 	let mp_mt = msid_of_mt mt in
@@ -38,7 +38,12 @@ let se_iter do_decl do_spec =
 	in
 	let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l')) in
 	mt_iter mt; do_decl (Dtype(r,l,t))
-    | MTwith (mt,_)->mt_iter mt
+    | MTwith (mt,ML_With_module(idl,mp))->
+        let mp_mt = msid_of_mt mt in
+        let mp_w =
+	  List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl
+	in
+	mt_iter mt; do_mp mp_w; do_mp mp
     | MTsig (_, sign) -> List.iter spec_iter sign
   and spec_iter = function
     | (_,Spec s) -> do_spec s
@@ -51,15 +56,16 @@ let se_iter do_decl do_spec =
 	me_iter m.ml_mod_expr; mt_iter m.ml_mod_type
     | (_,SEmodtype m) -> mt_iter m
   and me_iter = function
-    | MEident _ -> ()
+    | MEident mp -> do_mp mp
     | MEfunctor (_,mt,me) -> me_iter me; mt_iter mt
     | MEapply (me,me') -> me_iter me; me_iter me'
     | MEstruct (msid, sel) -> List.iter se_iter sel
   in
   se_iter
 
-let struct_iter do_decl do_spec s =
-  List.iter (function (_,sel) -> List.iter (se_iter do_decl do_spec) sel) s
+let struct_iter do_decl do_spec do_mp s =
+  List.iter
+    (function (_,sel) -> List.iter (se_iter do_decl do_spec do_mp) sel) s
 
 (*s Apply some fonctions upon all references in [ml_type], [ml_ast],
   [ml_decl], [ml_spec] and [ml_structure]. *)
@@ -141,7 +147,7 @@ let decl_ast_search f = function
   | _ -> ()
 
 let struct_ast_search f s =
-  try struct_iter (decl_ast_search f) (fun _ -> ()) s; false
+  try struct_iter (decl_ast_search f) (fun _ -> ()) (fun _ -> ()) s; false
   with Found -> true
 
 let rec type_search f = function
@@ -165,7 +171,9 @@ let spec_type_search f = function
   | Sval (_,u) -> type_search f u
 
 let struct_type_search f s =
-  try struct_iter (decl_type_search f) (spec_type_search f) s; false
+  try
+    struct_iter (decl_type_search f) (spec_type_search f) (fun _ -> ()) s;
+    false
   with Found -> true
 
 
@@ -247,34 +255,32 @@ let dfix_to_mlfix rv av i =
   let c = Array.map (subst 0) av
   in MLfix(i, ids, c)
 
+(* [optim_se] applies the [normalize] function everywhere and does the
+   inlining of code. The inlined functions are kept for the moment in
+   order to preserve the global interface, later [depcheck_se] will get
+   rid of them if possible *)
+
 let rec optim_se top to_appear s = function
   | [] -> []
   | (l,SEdecl (Dterm (r,a,t))) :: lse ->
       let a = normalize (ast_glob_subst !s a) in
       let i = inline r a in
       if i then s := Refmap'.add r a !s;
-      if top && i && not (library ()) && not (List.mem r to_appear)
-      then optim_se top to_appear s lse
-      else
-	let d = match optimize_fix a with
-	  | MLfix (0, _, [|c|]) ->
-	      Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|])
-	  | a -> Dterm (r, a, t)
-	in (l,SEdecl d) :: (optim_se top to_appear s lse)
+      let d = match optimize_fix a with
+	| MLfix (0, _, [|c|]) ->
+	  Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|])
+	| a -> Dterm (r, a, t)
+      in
+      (l,SEdecl d) :: (optim_se top to_appear s lse)
   | (l,SEdecl (Dfix (rv,av,tv))) :: lse ->
       let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in
-      let all = ref true in
       (* This fake body ensures that no fixpoint will be auto-inlined. *)
       let fake_body = MLfix (0,[||],[||]) in
       for i = 0 to Array.length rv - 1 do
 	if inline rv.(i) fake_body
 	then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s
-	else all := false
       done;
-      if !all && top && not (library ())
-	&& (array_for_all (fun r -> not (List.mem r to_appear)) rv)
-      then optim_se top to_appear s lse
-      else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
+      (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
   | (l,SEmodule m) :: lse ->
       let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr}
       in (l,SEmodule m) :: (optim_se top to_appear s lse)
@@ -289,7 +295,7 @@ and optim_me to_appear s = function
 
 (* After these optimisations, some dependencies may not be needed anymore.
    For non-library extraction, we recompute a minimal set of dependencies
-   for first-level objects *)
+   for first-level definitions (no module pruning yet). *)
 
 exception NoDepCheck
 
@@ -362,7 +368,7 @@ let rec depcheck_se = function
     end
   | t :: se ->
     let se' = depcheck_se se in
-    se_iter compute_deps_decl compute_deps_spec t;
+    se_iter compute_deps_decl compute_deps_spec add_needed_mp t;
     t :: se'
 
 let rec depcheck_struct = function
@@ -370,7 +376,7 @@ let rec depcheck_struct = function
   | (mp,lse)::struc ->
       let struc' = depcheck_struct struc in
       let lse' = depcheck_se lse in
-      (mp,lse')::struc'
+      if lse' = [] then struc' else (mp,lse')::struc'
 
 let check_implicits = function
   | MLexn s ->
@@ -389,9 +395,9 @@ let optimize_struct to_appear struc =
     List.map (fun (mp,lse) -> (mp, optim_se true (fst to_appear) subst lse))
       struc
   in
-  let opt_struc = List.filter (fun (_,lse) -> lse<>[]) opt_struc in
   ignore (struct_ast_search check_implicits opt_struc);
-  if library () then opt_struc
+  if library () then
+    List.filter (fun (_,lse) -> lse<>[]) opt_struc
   else begin
     reset_needed ();
     List.iter add_needed (fst to_appear);
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index c88c6669..43b08840 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -308,13 +308,14 @@ let build_constructors_of_type ind' argl =
 		    (Global.env ())
 		    construct
 		in
-		let argl =
-		  if argl = []
-		  then
+		let argl = match argl with
+                | None ->
  		    Array.to_list
-		      (Array.init (cst_narg - npar) (fun _ -> mkGHole ())
+		      (Array.init cst_narg (fun _ -> mkGHole ())
 		      )
-		  else argl
+                | Some l ->
+	            Array.to_list
+		      (Array.init npar (fun _ -> mkGHole ()))@l
 		in
 		let pat_as_term =
 		  mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
@@ -653,7 +654,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 			       Printer.pr_glob_constr b ++ str " in " ++
 			       Printer.pr_glob_constr rt ++ str ". try again with a cast")
 	in
-	let case_pats = build_constructors_of_type ind [] in
+	let case_pats = build_constructors_of_type ind None in
 	assert (Array.length case_pats = 2);
 	let brl =
 	  list_map_i
@@ -669,12 +670,12 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
     | GLetTuple(_,nal,_,b,e) ->
 	begin
 	  let nal_as_glob_constr =
-	    List.map
+	    Some (List.map
 	      (function
 		   Name id -> mkGVar id
 		 | Anonymous -> mkGHole ()
 	      )
-	      nal
+	      nal)
 	  in
 	  let b_as_constr = Pretyping.Default.understand Evd.empty env b in
 	  let b_typ = Typing.type_of env Evd.empty b_as_constr in
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 11d9a071..ab424c22 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -14,14 +14,14 @@ Delimit Scope Int_scope with I.
 
 Module Type Int.
 
-  Parameter int : Set.
+  Parameter t : Set.
 
-  Parameter zero : int.
-  Parameter one : int.
-  Parameter plus : int -> int -> int.
-  Parameter opp : int -> int.
-  Parameter minus : int -> int -> int.
-  Parameter mult : int -> int -> int.
+  Parameter zero : t.
+  Parameter one : t.
+  Parameter plus : t -> t -> t.
+  Parameter opp : t -> t.
+  Parameter minus : t -> t -> t.
+  Parameter mult : t -> t -> t.
 
   Notation "0" := zero : Int_scope.
   Notation "1" := one : Int_scope.
@@ -33,14 +33,14 @@ Module Type Int.
   Open Scope Int_scope.
 
   (* First, int is a ring: *)
-  Axiom ring : @ring_theory int 0 1 plus mult minus opp (@eq int).
+  Axiom ring : @ring_theory t 0 1 plus mult minus opp (@eq t).
 
   (* int should also be ordered: *)
 
-  Parameter le : int -> int -> Prop.
-  Parameter lt : int -> int -> Prop.
-  Parameter ge : int -> int -> Prop.
-  Parameter gt : int -> int -> Prop.
+  Parameter le : t -> t -> Prop.
+  Parameter lt : t -> t -> Prop.
+  Parameter ge : t -> t -> Prop.
+  Parameter gt : t -> t -> Prop.
   Notation "x <= y" := (le x y): Int_scope.
   Notation "x < y" := (lt x y) : Int_scope.
   Notation "x >= y" := (ge x y) : Int_scope.
@@ -61,7 +61,7 @@ Module Type Int.
    forall i j k, 0 < k -> i < j -> k*i<k*j.
 
   (* We should have a way to decide the equality and the order*)
-  Parameter compare : int -> int -> comparison.
+  Parameter compare : t -> t -> comparison.
   Infix "?=" := compare (at level 70, no associativity) : Int_scope.
   Axiom compare_Eq : forall i j, compare i j = Eq <-> i=j.
   Axiom compare_Lt : forall i j, compare i j = Lt <-> i<j.
@@ -83,7 +83,7 @@ Module Z_as_Int <: Int.
 
   Open Scope Z_scope.
 
-  Definition int := Z.
+  Definition t := Z.
   Definition zero := 0.
   Definition one := 1.
   Definition plus := Z.add.
@@ -91,7 +91,7 @@ Module Z_as_Int <: Int.
   Definition minus := Z.sub.
   Definition mult := Z.mul.
 
-  Lemma ring : @ring_theory int zero one plus mult minus opp (@eq int).
+  Lemma ring : @ring_theory t zero one plus mult minus opp (@eq t).
   Proof.
   constructor.
   exact Z.add_0_l.
@@ -138,6 +138,7 @@ End Z_as_Int.
 
 Module IntProperties (I:Int).
  Import I.
+ Local Notation int := I.t.
 
  (* Primo, some consequences of being a ring theory... *)
 
@@ -827,6 +828,7 @@ Module IntOmega (I:Int).
 Import I.
 Module IP:=IntProperties(I).
 Import IP.
+Local Notation int := I.t.
 
 (* \subsubsection{Definition of reified integer expressions}
    Terms are either:
@@ -1037,20 +1039,16 @@ Close Scope romega_scope.
 
 Theorem eq_term_true : forall t1 t2 : term, eq_term t1 t2 = true -> t1 = t2.
 Proof.
- simple induction t1; intros until t2; case t2; simpl in *;
- try (intros; discriminate; fail);
- [ intros; elim beq_true with (1 := H); trivial
- | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5;
-    elim H with (1 := H4); elim H0 with (1 := H5);
-    trivial
- | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5;
-    elim H with (1 := H4); elim H0 with (1 := H5);
-    trivial
- | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5;
-    elim H with (1 := H4); elim H0 with (1 := H5);
-    trivial
- | intros t21 H3; elim H with (1 := H3); trivial
- | intros; elim beq_nat_true with (1 := H); trivial ].
+ induction t1; destruct t2; simpl in *; try discriminate;
+ (rewrite andb_true_iff; intros (H1,H2)) || intros H; f_equal;
+ auto using beq_true, beq_nat_true.
+Qed.
+
+Theorem eq_term_refl : forall t0 : term, eq_term t0 t0 = true.
+Proof.
+ induction t0; simpl in *; try (apply andb_true_iff; split); trivial.
+ - now apply beq_iff.
+ - now apply beq_nat_true_iff.
 Qed.
 
 Ltac trivial_case := unfold not; intros; discriminate.
@@ -1058,31 +1056,7 @@ Ltac trivial_case := unfold not; intros; discriminate.
 Theorem eq_term_false :
  forall t1 t2 : term, eq_term t1 t2 = false -> t1 <> t2.
 Proof.
- simple induction t1;
- [ intros z t2; case t2; try trivial_case; simpl; unfold not;
-    intros; elim beq_false with (1 := H); simplify_eq H0;
-    auto
- | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl;
-    intros t21 t22 H3; unfold not; intro H4;
-    elim andb_false_elim with (1 := H3); intros H5;
-    [ elim H1 with (1 := H5); simplify_eq H4; auto
-    | elim H2 with (1 := H5); simplify_eq H4; auto ]
- | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl;
-    intros t21 t22 H3; unfold not; intro H4;
-    elim andb_false_elim with (1 := H3); intros H5;
-    [ elim H1 with (1 := H5); simplify_eq H4; auto
-    | elim H2 with (1 := H5); simplify_eq H4; auto ]
- | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl;
-    intros t21 t22 H3; unfold not; intro H4;
-    elim andb_false_elim with (1 := H3); intros H5;
-    [ elim H1 with (1 := H5); simplify_eq H4; auto
-    | elim H2 with (1 := H5); simplify_eq H4; auto ]
- | intros t11 H1 t2; case t2; try trivial_case; simpl; intros t21 H3;
-    unfold not; intro H4; elim H1 with (1 := H3);
-    simplify_eq H4; auto
- | intros n t2; case t2; try trivial_case; simpl; unfold not;
-    intros; elim beq_nat_false with (1 := H); simplify_eq H0;
-    auto ].
+ intros t1 t2 H E. subst t2. now rewrite eq_term_refl in H.
 Qed.
 
 (* \subsubsection{Tactiques pour éliminer ces tests}
@@ -1919,9 +1893,9 @@ Fixpoint fusion (trace : list t_fusion) (t : term) {struct trace} : term :=
       end
   end.
 
-Theorem fusion_stable : forall t : list t_fusion, term_stable (fusion t).
+Theorem fusion_stable : forall trace : list t_fusion, term_stable (fusion trace).
 Proof.
- simple induction t; simpl;
+ simple induction trace; simpl;
  [ exact reduce_stable
  | intros stp l H; case stp;
     [ apply compose_term_stable;
@@ -2093,11 +2067,8 @@ Definition constant_not_nul (i : nat) (h : hyps) :=
 Theorem constant_not_nul_valid :
  forall i : nat, valid_hyps (constant_not_nul i).
 Proof.
- unfold valid_hyps, constant_not_nul; intros;
- generalize (nth_valid ep e i lp); Simplify; simpl.
-
- elim_beq i1 i0; auto; simpl; intros H1 H2;
- elim H1; symmetry ; auto.
+ unfold valid_hyps, constant_not_nul; intros i ep e lp H.
+ generalize (nth_valid ep e i lp H); Simplify.
 Qed.
 
 (* \paragraph{[O_CONSTANT_NEG]} *)
@@ -2131,12 +2102,12 @@ Definition not_exact_divide (k1 k2 : int) (body : term)
   end.
 
 Theorem not_exact_divide_valid :
- forall (k1 k2 : int) (body : term) (t i : nat),
- valid_hyps (not_exact_divide k1 k2 body t i).
+ forall (k1 k2 : int) (body : term) (t0 i : nat),
+ valid_hyps (not_exact_divide k1 k2 body t0 i).
 Proof.
  unfold valid_hyps, not_exact_divide; intros;
  generalize (nth_valid ep e i lp); Simplify.
- rewrite (scalar_norm_add_stable t e), <-H1.
+ rewrite (scalar_norm_add_stable t0 e), <-H1.
  do 2 rewrite <- scalar_norm_add_stable; simpl in *; intros.
  absurd (interp_term e body * k1 + k2 = 0);
  [ now apply OMEGA4 | symmetry; auto ].
@@ -2509,9 +2480,9 @@ Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps :=
       execute_omega cont (apply_oper_2 i1 i2 (state m s) l)
   end.
 
-Theorem omega_valid : forall t : t_omega, valid_list_hyps (execute_omega t).
+Theorem omega_valid : forall tr : t_omega, valid_list_hyps (execute_omega tr).
 Proof.
- simple induction t; simpl;
+ simple induction tr; simpl;
  [ unfold valid_list_hyps; simpl; intros; left;
     apply (constant_not_nul_valid n ep e lp H)
  | unfold valid_list_hyps; simpl; intros; left;
@@ -2522,7 +2493,7 @@ Proof.
      (apply_oper_1_valid m (divide_and_approx k1 k2 body n)
         (divide_and_approx_valid k1 k2 body n) ep e lp H)
  | unfold valid_list_hyps; simpl; intros; left;
-    apply (not_exact_divide_valid i i0 t0 n n0 ep e lp H)
+    apply (not_exact_divide_valid _ _ _ _ _ ep e lp H)
  | unfold valid_list_hyps, valid_hyps;
     intros k body n t' Ht' m ep e lp H; apply Ht';
     apply
@@ -2618,10 +2589,10 @@ Qed.
 (* \subsubsection{Exécution de la trace} *)
 
 Theorem execute_goal :
- forall (t : t_omega) (ep : list Prop) (env : list int) (l : hyps),
- interp_list_goal ep env (execute_omega t l) -> interp_goal ep env l.
+ forall (tr : t_omega) (ep : list Prop) (env : list int) (l : hyps),
+ interp_list_goal ep env (execute_omega tr l) -> interp_goal ep env l.
 Proof.
- intros; apply (goal_valid (execute_omega t) (omega_valid t) ep env l H).
+ intros; apply (goal_valid (execute_omega tr) (omega_valid tr) ep env l H).
 Qed.
 
 
@@ -2936,13 +2907,13 @@ Proof.
     | intro; apply ne_left_2; assumption ]
  | case p; simpl; intros; auto; generalize H; elim (t_rewrite_stable s);
     simpl; intro H1;
-    [ rewrite (plus_0_r_reverse (interp_term e t0)); rewrite H1;
+    [ rewrite (plus_0_r_reverse (interp_term e t1)); rewrite H1;
        rewrite plus_permute; rewrite plus_opp_r;
        rewrite plus_0_r; trivial
-    | apply (fun a b => plus_le_reg_r a b (- interp_term e t));
+    | apply (fun a b => plus_le_reg_r a b (- interp_term e t0));
        rewrite plus_opp_r; assumption
     | rewrite ge_le_iff;
-       apply (fun a b => plus_le_reg_r a b (- interp_term e t0));
+       apply (fun a b => plus_le_reg_r a b (- interp_term e t1));
        rewrite plus_opp_r; assumption
     | rewrite gt_lt_iff; apply lt_left_inv; assumption
     | apply lt_left_inv; assumption
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 6a5878b3..dfcc8526 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -663,6 +663,7 @@ let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce)
 let admit_obligations n =
   let prg = get_prog_err n in
   let obls, rem = prg.prg_obligations in
+  let obls = Array.copy obls in
     Array.iteri 
       (fun i x ->
 	match x.obl_body with