- Parameterize unification by two sets of transparent_state, one for open

term unification (for constant and variable delta unfolding) and one to
parameterize closed-term conversion. Most of the time conversion uses
full delta and unification does no delta. This fine-grain is used in
rewrite/setoid_rewrite, where only closed-term delta on global constants
is allowed.
- Interpret Hint Unfold as a directive for delta conversion in
auto/eauto when applying lemmas (i.e., for Resolve and Immediate hints).
- Remove ad-hoc support for this in typeclasses. Now setoid_rewrite
works correctly w.r.t. the old version regarding local definitions.
- Fix closed bugs which needed updating due to syntax modifications.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10824 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 20 insertions, 22 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f11ed36da..c5e9dff8b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -117,31 +117,28 @@ let sort_eqns = unify_r2l
 *)
 
 type unify_flags = { 
-  modulo_conv_on_closed_terms : bool; 
+  modulo_conv_on_closed_terms : Names.transparent_state option;
   use_metas_eagerly : bool;
-  modulo_delta : Cpred.t;
-  modulo_zeta : bool;
+  modulo_delta : Names.transparent_state;
 }
 
 let default_unify_flags = {
-  modulo_conv_on_closed_terms = true;
+  modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = true;
-  modulo_delta = Cpred.full;
-  modulo_zeta = true;
+  modulo_delta = full_transparent_state;
 }
 
 let default_no_delta_unify_flags = {
-  modulo_conv_on_closed_terms = true;
+  modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = true;
-  modulo_delta = Cpred.empty;
-  modulo_zeta = true;
+  modulo_delta = empty_transparent_state;
 }
 
 let expand_constant env flags c = 
   let (ids,csts) = Conv_oracle.freeze() in
   match kind_of_term c with
-  | Const cst when Cpred.mem cst csts && Cpred.mem cst flags.modulo_delta -> constant_opt_value env cst
-  | Var id when flags.modulo_zeta && Idpred.mem id ids -> named_body id env
+  | Const cst when Cpred.mem cst csts && Cpred.mem cst (snd flags.modulo_delta) -> constant_opt_value env cst
+  | Var id when Idpred.mem id ids && Idpred.mem id (fst flags.modulo_delta) -> named_body id env
   | _ -> None
 
 let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n =
@@ -149,9 +146,10 @@ let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n =
   let trivial_unify pb (metasubst,_) m n =
     match subst_defined_metas metas m with
     | Some m ->
-	if flags.modulo_conv_on_closed_terms 
-	then is_fconv (conv_pb_of pb) env sigma m n
-	else eq_constr m n
+	(match flags.modulo_conv_on_closed_terms with
+	    Some flags ->
+	      is_trans_fconv (conv_pb_of pb) flags env sigma m n
+	  | None -> eq_constr m n)
     | _ -> false in
   let rec unirec_rec curenv pb b ((metasubst,evarsubst) as substn) curm curn =
     let cM = Evarutil.whd_castappevar sigma curm
@@ -224,7 +222,7 @@ let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n =
 
   and expand curenv pb b substn cM f1 l1 cN f2 l2 =
     if trivial_unify pb substn cM cN then substn
-    else if b & not (Cpred.is_empty flags.modulo_delta) then
+    else if b then
       match expand_constant curenv flags f1 with
       | Some c ->
 	  unirec_rec curenv pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN
@@ -239,9 +237,10 @@ let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n =
 
   in
     if (not(occur_meta m)) &&
-      (if flags.modulo_conv_on_closed_terms
-       then is_fconv (conv_pb_of cv_pb) env sigma m n
-       else eq_constr m n)
+      (match flags.modulo_conv_on_closed_terms with
+	  Some flags ->
+	    is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n
+	| None -> eq_constr m n)
     then 
       (metas,[])
     else 
@@ -637,7 +636,7 @@ let w_unify_to_subterm_list env flags allow_K oplist t evd =
 
 let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
   (* Remove delta when looking for a subterm *)
-  let flags = { flags with modulo_delta = Cpred.empty } in
+  let flags = { flags with modulo_delta = (fst flags.modulo_delta, Cpred.empty) } in
   let (evd',cllist) =
     w_unify_to_subterm_list env flags allow_K oplist typ evd in
   let typp = Typing.meta_type evd' p in
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 8e8168e5c..9156623f5 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -15,10 +15,9 @@ open Evd
 (*i*)
 
 type unify_flags = { 
-  modulo_conv_on_closed_terms : bool; 
+  modulo_conv_on_closed_terms : Names.transparent_state option; 
   use_metas_eagerly : bool;
-  modulo_delta : Names.Cpred.t;
-  modulo_zeta : bool;
+  modulo_delta : Names.transparent_state;
 }
 
 val default_unify_flags : unify_flags