Reverting the following block of three commits:

- Registering strict implicit arguments systematically (35fc7d728168)
- Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6)
- Fixing Coq compilation (894a3d16471)

Systematically computing strict implicit arguments can lead to big
computations, so I suspend this attempt, waiting for improved
computation of implicit arguments, or alternative heuristics going
toward having more conversion in rewrite.

7 files changed, 84 insertions, 130 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index ec362b538..2e61cb697 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -144,7 +144,6 @@ Program
 Coercion
 Cases
 Pretyping
-Impargs
 Unification
 Declaremods
 Library
diff --git a/interp/interp.mllib b/interp/interp.mllib
index d3b7077c4..c9a031526 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -10,6 +10,7 @@ Dumpglob
 Syntax_def
 Smartlocate
 Reserve
+Impargs
 Implicit_quantifiers
 Constrintern
 Modintern
diff --git a/library/impargs.ml b/library/impargs.ml
index e3c5c84b0..d88d6f106 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -268,9 +268,6 @@ let compute_implicits_names env t =
   let _, impls = compute_implicits_gen false false false false true env t in
   List.map fst impls
 
-let compute_implicits_strict env t =
-  List.map snd (snd (compute_implicits_gen true true true true false env t))
-
 (* Extra information about implicit arguments *)
 
 type maximal_insertion = bool (* true = maximal contextual insertion *)
@@ -396,16 +393,14 @@ let set_manual_implicits env flags enriching autoimps l =
   merge 1 l autoimps
 
 let compute_semi_auto_implicits env f manual t =
-  let strictimpls = compute_implicits_strict env t in
-  let auto = match manual with
+  match manual with
   | [] ->
       if not f.auto then [DefaultImpArgs, []]
       else let _,l = compute_implicits_flags env f false t in
 	     [DefaultImpArgs, prepare_implicits f l]
   | _ ->
       let _,autoimpls = compute_auto_implicits env f f.auto t in
-      [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual] in
-  strictimpls,auto
+      [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual]
 
 (*s Constants. *)
 
@@ -488,21 +483,9 @@ type implicit_discharge_request =
 
 let implicits_table = Summary.ref Refmap.empty ~name:"implicits"
 
-let strict_implicits_of_global n ref =
-  try
-    let impls = fst (Refmap.find ref !implicits_table) in
-    let status = List.map (function
-    | Some (DepRigid (Hyp k) | DepFlexAndRigid (_,Hyp k)) -> k <= n
-    | _ -> false) impls in
-    let m = List.length status in
-    if m > n then fst (List.chop n status)
-    else if m < n then status @ List.make (n-m) false
-    else status
-  with Not_found -> anomaly (str "No strict implicit arguments." ++ Nametab.pr_global_env Idset.empty ref)
-
 let implicits_of_global ref =
   try
-    let l = snd (Refmap.find ref !implicits_table) in
+    let l = Refmap.find ref !implicits_table in
     try
       let rename_l = Arguments_renaming.arguments_names ref in
       let rename imp name = match imp, name with
@@ -530,14 +513,14 @@ let subst_implicits (subst,(req,l)) =
 
 let impls_of_context ctx =
   let map (id, impl, _, _) = match impl with
-  | Implicit -> Some (* dummy *) Manual, Some (id, Manual, (true, true))
-  | _ -> None, None
+  | Implicit -> Some (id, Manual, (true, true))
+  | _ -> None
   in
   let is_set (_, _, b, _) = match b with
   | None -> true
   | Some _ -> false
   in
-  List.split (List.rev_map map (List.filter is_set ctx))
+  List.rev_map map (List.filter is_set ctx)
 
 let section_segment_of_reference = function
   | ConstRef con -> pi1 (section_segment_of_constant con)
@@ -560,33 +543,26 @@ let discharge_implicits (_,(req,l)) =
     (try
       let vars = section_segment_of_reference ref in
       let ref' = if isVarRef ref then ref else pop_global_reference ref in
-      let extrastrict, extra_impls = impls_of_context vars in
-      let oldstrict,oldimpls = snd (List.hd l) in
-      let newstrict = extrastrict @ oldstrict in
-      let newimpls = List.map (add_section_impls vars extra_impls) oldimpls in
-      let l' = [ref',(newstrict,newimpls)] in
+      let extra_impls = impls_of_context vars in
+      let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
       Some (ImplInteractive (ref',flags,exp),l')
     with Not_found -> (* ref not defined in this section *) Some (req,l))
   | ImplConstant (con,flags) ->
     (try
       let con' = pop_con con in
       let vars,_,_ = section_segment_of_constant con in
-      let extrastrict, extra_impls = impls_of_context vars in
-      let oldstrict,oldimpls = snd (List.hd l) in
-      let newstrict = extrastrict @ oldstrict in
-      let newimpls = List.map (add_section_impls vars extra_impls) oldimpls in
-      let l' = [ConstRef con',(newstrict,newimpls)] in
+      let extra_impls = impls_of_context vars in
+      let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in
+      let l' = [ConstRef con',newimpls] in
 	Some (ImplConstant (con',flags),l')
     with Not_found -> (* con not defined in this section *) Some (req,l))
   | ImplMutualInductive (kn,flags) ->
     (try
-      let l' = List.map (fun (gr, (newstrict,l)) ->
+      let l' = List.map (fun (gr, l) ->
 	let vars = section_segment_of_reference gr in
-        let extrastrict, extra_impls = impls_of_context vars in
-        let newstrict = extrastrict @ newstrict in
-        let newimpls = List.map (add_section_impls vars extra_impls) l in
+	let extra_impls = impls_of_context vars in
 	((if isVarRef gr then gr else pop_global_reference gr),
-	 (newstrict,newimpls))) l
+	 List.map (add_section_impls vars extra_impls) l)) l
       in
 	Some (ImplMutualInductive (pop_kn kn,flags),l')
     with Not_found -> (* ref not defined in this section *) Some (req,l))
@@ -595,16 +571,15 @@ let rebuild_implicits (req,l) =
   match req with
   | ImplLocal -> assert false
   | ImplConstant (con,flags) ->
-      let _,oldimpls = snd (List.hd l) in
-      let newstrict,newimpls = compute_constant_implicits flags [] con in
-      req, [ConstRef con, (newstrict,List.map2 merge_impls oldimpls newimpls)]
+      let oldimpls = snd (List.hd l) in
+      let newimpls = compute_constant_implicits flags [] con in
+      req, [ConstRef con, List.map2 merge_impls oldimpls newimpls]
   | ImplMutualInductive (kn,flags) ->
       let newimpls = compute_all_mib_implicits flags [] kn in
       let rec aux olds news =
 	match olds, news with
-	| (_, (_,oldimpls)) :: old, (gr, (newstrict,newimpls)) :: tl ->
-	    (gr, (newstrict,List.map2 merge_impls oldimpls newimpls))
-            :: aux old tl
+	| (_, oldimpls) :: old, (gr, newimpls) :: tl ->
+	    (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl
 	| [], [] -> []
 	| _, _ -> assert false
       in req, aux l newimpls
@@ -613,19 +588,18 @@ let rebuild_implicits (req,l) =
       (if isVarRef ref && is_in_section ref then ImplLocal else req),
       match o with
       | ImplAuto ->
-	  let _,oldimpls = snd (List.hd l) in
-	  let newstrict,newimpls = compute_global_implicits flags [] ref in
-	    [ref,(newstrict,List.map2 merge_impls oldimpls newimpls)]
+	  let oldimpls = snd (List.hd l) in
+	  let newimpls = compute_global_implicits flags [] ref in
+	    [ref,List.map2 merge_impls oldimpls newimpls]
       | ImplManual userimplsize ->
-	  let _,oldimpls = snd (List.hd l) in
-	  let newstrict,newimpls = compute_global_implicits flags [] ref in
-          let newimpls = List.hd newimpls in
+	  let oldimpls = snd (List.hd l) in
 	  if flags.auto then
+	    let newimpls = List.hd (compute_global_implicits flags [] ref) in
 	    let p = List.length (snd newimpls) - userimplsize in
 	    let newimpls = on_snd (List.firstn p) newimpls in
-	    [ref,(newstrict,List.map (fun o -> merge_impls o newimpls) oldimpls)]
+	    [ref,List.map (fun o -> merge_impls o newimpls) oldimpls]
 	  else
-	    [ref,(newstrict,oldimpls)]
+	    [ref,oldimpls]
 
 let classify_implicits (req,_ as obj) = match req with
 | ImplLocal -> Dispose
@@ -633,8 +607,7 @@ let classify_implicits (req,_ as obj) = match req with
 
 type implicits_obj =
     implicit_discharge_request *
-      (global_reference *
-         (implicit_explanation option list * implicits_list list)) list
+      (global_reference * implicits_list list) list
 
 let inImplicits : implicits_obj -> obj =
   declare_object {(default_object "IMPLICITS") with
@@ -719,12 +692,11 @@ let declare_manual_implicits local ref ?enriching l =
 	List.map (fun (imps,n) ->
 	  (LessArgsThan (nargs-n),
 	   set_manual_implicits env flags enriching autoimpls imps)) l in
-  let strictimpls = compute_implicits_strict env t in
   let req =
     if is_local local ref then ImplLocal
     else ImplInteractive(ref,flags,ImplManual (List.length autoimpls))
   in
-    add_anonymous_leaf (inImplicits (req,[ref,(strictimpls,l')]))
+    add_anonymous_leaf (inImplicits (req,[ref,l']))
 
 let maybe_declare_manual_implicits local ref ?enriching l =
   match l with
diff --git a/library/impargs.mli b/library/impargs.mli
index 3ba928508..297145f09 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -120,8 +120,6 @@ val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool
 
 val implicits_of_global : global_reference -> implicits_list list
 
-val strict_implicits_of_global : int -> global_reference -> bool list
-
 val extract_impargs_data :
   implicits_list list -> ((int * int) option * implicit_status list) list
 
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 2958b9e73..b189360c0 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -31,5 +31,4 @@ Detyping
 Indrec
 Cases
 Pretyping
-Impargs
 Unification
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fa419ddaf..8009bad2d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -592,7 +592,7 @@ let eta_constructor_app env f l1 term =
   | _ -> assert false
 
 let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n =
-  let rec unirec_rec (curenv,nb as curenvnb) pb opt flags ((sigma,metasubst,evarsubst) as substn) curm curn =
+  let rec unirec_rec (curenv,nb as curenvnb) pb opt ((sigma,metasubst,evarsubst) as substn) curm curn =
     let cM = Evarutil.whd_head_evar sigma curm
     and cN = Evarutil.whd_head_evar sigma curn in
     let () = 
@@ -678,28 +678,28 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
                error_cannot_unify curenv sigma (m,n))
 
 	| Lambda (na,t1,c1), Lambda (_,t2,c2) ->
-	    unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} flags
-	      (unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} flags substn t1 t2) c1 c2
+	    unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true}
+	      (unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn t1 t2) c1 c2
 	| Prod (na,t1,c1), Prod (_,t2,c2) ->
-	    unirec_rec (push (na,t1) curenvnb) pb {opt with at_top = true} flags
-	      (unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} flags substn t1 t2) c1 c2
-	| LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb opt flags substn (subst1 a c) cN
-	| _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt flags substn cM (subst1 a c)
+	    unirec_rec (push (na,t1) curenvnb) pb {opt with at_top = true}
+	      (unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn t1 t2) c1 c2
+	| LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb opt substn (subst1 a c) cN
+	| _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c)
 
 	(** Fast path for projections. *)
 	| Proj (p1,c1), Proj (p2,c2) when eq_constant
 	    (Projection.constant p1) (Projection.constant p2) ->
-	  (try unify_same_proj curenvnb cv_pb {opt with at_top = true} flags
+	  (try unify_same_proj curenvnb cv_pb {opt with at_top = true}
 	       substn c1 c2
 	   with ex when precatchable_exception ex ->
-	     unify_not_same_head curenvnb pb opt flags substn cM cN)
+	     unify_not_same_head curenvnb pb opt substn cM cN)
 
         (* eta-expansion *)
 	| Lambda (na,t1,c1), _ when flags.modulo_eta ->
-	    unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} flags substn
+	    unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} substn
 	      c1 (mkApp (lift 1 cN,[|mkRel 1|]))
 	| _, Lambda (na,t2,c2) when flags.modulo_eta ->
-	    unirec_rec (push (na,t2) curenvnb) CONV {opt with at_top = true} flags substn
+	    unirec_rec (push (na,t2) curenvnb) CONV {opt with at_top = true} substn
 	      (mkApp (lift 1 cM,[|mkRel 1|])) c2
 
 	(* For records *)
@@ -710,7 +710,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	  (try 
 	     let l1', l2' = eta_constructor_app curenv f1 l1 cN in
 	     let opt' = {opt with at_top = true; with_cs = false} in
-	       Array.fold_left2 (unirec_rec curenvnb CONV opt' flags) substn l1' l2'
+	       Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2'
 	   with ex when precatchable_exception ex ->
 	     match kind_of_term cN with
 	     | App(f2,l2) when isMeta f2 || isEvar f2 ->
@@ -722,7 +722,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	  (try 
 	     let l2', l1' = eta_constructor_app curenv f2 l2 cM in
 	     let opt' = {opt with at_top = true; with_cs = false} in
-	       Array.fold_left2 (unirec_rec curenvnb CONV opt' flags) substn l1' l2'
+	       Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2'
 	   with ex when precatchable_exception ex ->
 	     match kind_of_term cM with
 	     | App(f1,l1) when isMeta f1 || isEvar f1 ->
@@ -732,12 +732,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
             (try 
 	     let opt' = {opt with at_top = true; with_types = false} in
-	       Array.fold_left2 (unirec_rec curenvnb CONV {opt with at_top = true} flags)
-	       (unirec_rec curenvnb CONV opt' flags
-		(unirec_rec curenvnb CONV opt' flags substn p1 p2) c1 c2)
+	       Array.fold_left2 (unirec_rec curenvnb CONV {opt with at_top = true})
+	       (unirec_rec curenvnb CONV opt'
+		(unirec_rec curenvnb CONV opt' substn p1 p2) c1 c2)
                  cl1 cl2
 	     with ex when precatchable_exception ex ->
-	       reduce curenvnb pb opt flags substn cM cN)
+	       reduce curenvnb pb opt substn cM cN)
 
 	| App (f1,l1), _ when 
 	    (isMeta f1 && use_metas_pattern_unification flags nb l1
@@ -749,7 +749,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
                  (match kind_of_term cN with
                  | App (f2,l2) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
                  | Proj _ -> unify_app curenvnb pb opt substn cM f1 l1 cN cN [||]
-                 | _ -> unify_not_same_head curenvnb pb opt flags substn cM cN)
+                 | _ -> unify_not_same_head curenvnb pb opt substn cM cN)
              | Some l ->
                  solve_pattern_eqn_array curenvnb f1 l cN substn)
 
@@ -763,7 +763,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
                  (match kind_of_term cM with
                  | App (f1,l1) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
                  | Proj _ -> unify_app curenvnb pb opt substn cM cM [||] cN f2 l2
-                 | _ -> unify_not_same_head curenvnb pb opt flags substn cM cN)
+                 | _ -> unify_not_same_head curenvnb pb opt substn cM cN)
              | Some l ->
 	         solve_pattern_eqn_array curenvnb f2 l cM substn)
 
@@ -777,7 +777,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	  unify_app curenvnb pb opt substn cM cM [||] cN f2 l2
 
 	| _ ->
-          unify_not_same_head curenvnb pb opt flags substn cM cN
+          unify_not_same_head curenvnb pb opt substn cM cN
 
   and unify_app (curenv, nb as curenvnb) pb opt (sigma, metas, evars as substn) cM f1 l1 cN f2 l2 =
     try
@@ -801,32 +801,20 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
       let f2, l2 = expand_proj f2 f1 l2 in
       let opta = {opt with at_top = true; with_types = false} in
       let optf = {opt with at_top = true; with_types = true} in
-      let same_glob f1 f2 =
-        try Globnames.RefOrdered.equal (Globnames.global_of_constr f1) (Globnames.global_of_constr f2) && not (isVar f1)
-        with Not_found -> false in
-      if same_glob f1 f2 && Int.equal (Array.length l1) (Array.length l2) then
-        let impls =
-          Impargs.strict_implicits_of_global (Array.length l1) (Globnames.global_of_constr f1) in
-	  Array.fold_left3
-            (fun subst b -> unirec_rec curenvnb CONV optf
-              (if b then default_core_unify_flags () else flags) subst)
-              (unirec_rec curenvnb CONV optf flags substn f1 f2)
-              (Array.of_list impls) l1 l2
-      else
       let (f1,l1,f2,l2) = adjust_app_array_size f1 l1 f2 l2 in
 	if Array.length l1 == 0 then error_cannot_unify (fst curenvnb) sigma (cM,cN)
 	else
-	  Array.fold_left2 (unirec_rec curenvnb CONV opta flags)
-	    (unirec_rec curenvnb CONV optf flags substn f1 f2) l1 l2
+	  Array.fold_left2 (unirec_rec curenvnb CONV opta)
+	    (unirec_rec curenvnb CONV optf substn f1 f2) l1 l2
     with ex when precatchable_exception ex ->
-    try reduce curenvnb pb {opt with with_types = false} flags substn cM cN
+    try reduce curenvnb pb {opt with with_types = false} substn cM cN
     with ex when precatchable_exception ex ->
-    try canonical_projections curenvnb pb opt flags cM cN substn
+    try canonical_projections curenvnb pb opt cM cN substn
     with ex when precatchable_exception ex ->
-    expand curenvnb pb {opt with with_types = false} flags substn cM f1 l1 cN f2 l2
+    expand curenvnb pb {opt with with_types = false} substn cM f1 l1 cN f2 l2
 
-  and unify_same_proj (curenv, nb as curenvnb) cv_pb opt flags substn c1 c2 =
-    let substn = unirec_rec curenvnb CONV opt flags substn c1 c2 in
+  and unify_same_proj (curenv, nb as curenvnb) cv_pb opt substn c1 c2 =
+    let substn = unirec_rec curenvnb CONV opt substn c1 c2 in
       try (* Force unification of the types to fill in parameters *)
 	let ty1 = get_type_of curenv ~lax:true sigma c1 in
 	let ty2 = get_type_of curenv ~lax:true sigma c2 in
@@ -838,33 +826,33 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	    ty1 ty2
       with RetypeError _ -> substn
 
-  and unify_not_same_head curenvnb pb opt flags (sigma, metas, evars as substn) cM cN =
-    try canonical_projections curenvnb pb opt flags cM cN substn
+  and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn) cM cN =
+    try canonical_projections curenvnb pb opt cM cN substn
     with ex when precatchable_exception ex ->
     let sigma', b = constr_cmp cv_pb sigma flags cM cN in
       if b then (sigma', metas, evars)
       else
-	try reduce curenvnb pb opt flags substn cM cN
+	try reduce curenvnb pb opt substn cM cN
 	with ex when precatchable_exception ex ->
 	let (f1,l1) =
 	  match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in
 	let (f2,l2) =
 	  match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in
-	  expand curenvnb pb opt flags substn cM f1 l1 cN f2 l2
+	  expand curenvnb pb opt substn cM f1 l1 cN f2 l2
 
-  and reduce curenvnb pb opt flags (sigma, metas, evars as substn) cM cN =
+  and reduce curenvnb pb opt (sigma, metas, evars as substn) cM cN =
     if use_full_betaiota flags && not (subterm_restriction opt flags) then
       let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in
 	if not (Term.eq_constr cM cM') then
-	  unirec_rec curenvnb pb opt flags substn cM' cN
+	  unirec_rec curenvnb pb opt substn cM' cN
 	else
 	  let cN' = do_reduce flags.modulo_delta curenvnb sigma cN in
 	    if not (Term.eq_constr cN cN') then
-	      unirec_rec curenvnb pb opt flags substn cM cN'
+	      unirec_rec curenvnb pb opt substn cM cN'
 	    else error_cannot_unify (fst curenvnb) sigma (cM,cN)
     else error_cannot_unify (fst curenvnb) sigma (cM,cN)
 	    
-  and expand (curenv,_ as curenvnb) pb opt flags (sigma,metasubst,evarsubst as substn) cM f1 l1 cN f2 l2 =
+  and expand (curenv,_ as curenvnb) pb opt (sigma,metasubst,evarsubst as substn) cM f1 l1 cN f2 l2 =
     let res =
       (* Try full conversion on meta-free terms. *)
       (* Back to 1995 (later on called trivial_unify in 2002), the
@@ -906,35 +894,35 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	| Some true ->
 	    (match expand_key flags.modulo_delta curenv sigma cf1 with
 	    | Some c ->
-		unirec_rec curenvnb pb opt flags substn
+		unirec_rec curenvnb pb opt substn
                   (whd_betaiotazeta sigma (mkApp(c,l1))) cN
 	    | None ->
 		(match expand_key flags.modulo_delta curenv sigma cf2 with
 		| Some c ->
-		    unirec_rec curenvnb pb opt flags substn cM
+		    unirec_rec curenvnb pb opt substn cM
                       (whd_betaiotazeta sigma (mkApp(c,l2)))
 		| None ->
 		    error_cannot_unify curenv sigma (cM,cN)))
 	| Some false ->
 	    (match expand_key flags.modulo_delta curenv sigma cf2 with
 	    | Some c ->
-		unirec_rec curenvnb pb opt flags substn cM
+		unirec_rec curenvnb pb opt substn cM
                   (whd_betaiotazeta sigma (mkApp(c,l2)))
 	    | None ->
 		(match expand_key flags.modulo_delta curenv sigma cf1 with
 		| Some c ->
-		    unirec_rec curenvnb pb opt flags substn
+		    unirec_rec curenvnb pb opt substn
                       (whd_betaiotazeta sigma (mkApp(c,l1))) cN
 		| None ->
 		    error_cannot_unify curenv sigma (cM,cN)))
 
-  and canonical_projections (curenv, _ as curenvnb) pb opt flags cM cN (sigma,_,_ as substn) =
+  and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) =
     let f1 () =
       if isApp cM then
 	let f1l1 = whd_nored_state sigma (cM,Stack.empty) in
 	  if is_open_canonical_projection curenv sigma f1l1 then
 	    let f2l2 = whd_nored_state sigma (cN,Stack.empty) in
-	      solve_canonical_projection curenvnb pb opt flags cM f1l1 cN f2l2 substn
+	      solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn
 	  else error_cannot_unify (fst curenvnb) sigma (cM,cN)
       else error_cannot_unify (fst curenvnb) sigma (cM,cN)
     in
@@ -950,11 +938,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	    let f2l2 = whd_nored_state sigma (cN, Stack.empty) in
 	      if is_open_canonical_projection curenv sigma f2l2 then
 		let f1l1 = whd_nored_state sigma (cM, Stack.empty) in
-		  solve_canonical_projection curenvnb pb opt flags cN f2l2 cM f1l1 substn
+		  solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn
 	      else error_cannot_unify (fst curenvnb) sigma (cM,cN)
 	  else error_cannot_unify (fst curenvnb) sigma (cM,cN)
 
-  and solve_canonical_projection curenvnb pb opt flags cM f1l1 cN f2l2 (sigma,ms,es) =
+  and solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 (sigma,ms,es) =
     let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
       try Evarconv.check_conv_record f1l1 f2l2
       with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -973,15 +961,15 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
       try
       let opt' = {opt with with_types = false} in
       let (substn,_,_) = Reductionops.Stack.fold2
-			   (fun s u1 u -> unirec_rec curenvnb pb opt' flags s u1 (substl ks u))
+			   (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u))
 			   (evd,ms,es) us2 us in
       let (substn,_,_) = Reductionops.Stack.fold2
-			   (fun s u1 u -> unirec_rec curenvnb pb opt' flags s u1 (substl ks u))
+			   (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u))
 			   substn params1 params in
-      let (substn,_,_) = Reductionops.Stack.fold2 (unirec_rec curenvnb pb opt' flags ) substn ts ts1 in
+      let (substn,_,_) = Reductionops.Stack.fold2 (unirec_rec curenvnb pb opt') substn ts ts1 in
       let app = mkApp (c, Array.rev_of_list ks) in
       (* let substn = unirec_rec curenvnb pb b false substn t cN in *)
-	unirec_rec curenvnb pb opt' flags substn c1 app
+	unirec_rec curenvnb pb opt' substn c1 app
       with Invalid_argument "Reductionops.Stack.fold2" ->
 	error_cannot_unify (fst curenvnb) sigma (cM,cN)
     else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -1007,8 +995,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
   try
     let a = match res with 
     | Some sigma -> sigma, ms, es
-    | None -> unirec_rec (env,0) cv_pb opt flags subst m n
-    in
+    | None -> unirec_rec (env,0) cv_pb opt subst m n in
     if !debug_unification then msg_debug (str "Leaving unification with success");
     a
   with e ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a7fc38a23..d6083860a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -170,9 +170,8 @@ let instantiate_lemma gl c ty l l2r concl =
   let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in
    [eqclause]
 
-let rewrite_conv_closed_core_unif_flags env =
-  let ts = Conv_oracle.get_transp_state (Environ.oracle env) in {
-  modulo_conv_on_closed_terms = Some ts;
+let rewrite_conv_closed_core_unif_flags = {
+  modulo_conv_on_closed_terms = Some full_transparent_state;
     (* We have this flag for historical reasons, it has e.g. the consequence *)
     (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *)
 
@@ -198,18 +197,17 @@ let rewrite_conv_closed_core_unif_flags env =
   modulo_eta = true;
 }
 
-let rewrite_conv_closed_unif_flags env =
-  let flags = rewrite_conv_closed_core_unif_flags env in {
-  core_unify_flags = flags;
-  merge_unify_flags = flags;
-  subterm_unify_flags = flags;
+let rewrite_conv_closed_unif_flags = {
+  core_unify_flags = rewrite_conv_closed_core_unif_flags;
+  merge_unify_flags = rewrite_conv_closed_core_unif_flags;
+  subterm_unify_flags = rewrite_conv_closed_core_unif_flags;
   allow_K_in_toplevel_higher_order_unification = false;
   resolve_evars = false
 }
 
 let rewrite_elim with_evars frzevars cls c e =
   Proofview.Goal.enter begin fun gl ->
-  let flags = make_flags frzevars (Proofview.Goal.sigma gl) (rewrite_conv_closed_unif_flags (Proofview.Goal.env gl)) c in
+  let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_conv_closed_unif_flags c in
   general_elim_clause with_evars flags cls c e
   end