Add a flag to control betaiota reduction during unification to maintain backward compatibility.

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

9 files changed, 57 insertions, 36 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 7d5d68fbb1..d226c94d1d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -171,6 +171,7 @@ type unify_flags = {
   modulo_delta_types : Names.transparent_state;
   resolve_evars : bool;
   use_evars_pattern_unification : bool;
+  modulo_betaiota : bool;
   modulo_eta : bool
 }
 
@@ -181,6 +182,7 @@ let default_unify_flags = {
   modulo_delta_types = full_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = true;
+  modulo_betaiota = false;
   modulo_eta = true
 }
 
@@ -191,6 +193,7 @@ let default_no_delta_unify_flags = {
   modulo_delta_types = full_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = false;
+  modulo_betaiota = false;
   modulo_eta = true
 }
 
@@ -342,14 +345,17 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 		    expand curenvnb pb b substn cM f1 l1 cN f2 l2
 
   and reduce curenvnb pb b (sigma, metas, evars as substn) cM cN =
-    let cM' = do_reduce (fst curenvnb) sigma cM in
-      if not (eq_constr cM cM') then
-	unirec_rec curenvnb pb true substn cM' cN
-      else
-	let cN' = do_reduce (fst curenvnb) sigma cN in
-	  if not (eq_constr cN cN') then
-	    unirec_rec curenvnb pb true substn cM cN'
-	  else error_cannot_unify (fst curenvnb) sigma (cM,cN)
+    if flags.modulo_betaiota then
+      let cM' = do_reduce (fst curenvnb) sigma cM in
+	if not (eq_constr cM cM') then
+	  unirec_rec curenvnb pb true substn cM' cN
+	else
+	  let cN' = do_reduce (fst curenvnb) sigma cN in
+	    if not (eq_constr cN cN') then
+	      unirec_rec curenvnb pb true 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 b (sigma,metasubst,_ as substn) cM f1 l1 cN f2 l2 =
 
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 0462688b43..cd8e70418a 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -17,6 +17,7 @@ type unify_flags = {
   modulo_delta_types : Names.transparent_state;
   resolve_evars : bool;
   use_evars_pattern_unification : bool;
+  modulo_betaiota : bool;
   modulo_eta : bool
 }
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 13eda91569..e4ad27f2e5 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -108,6 +108,7 @@ let fail_quick_unif_flags = {
   modulo_delta_types = full_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = false;
+  modulo_betaiota = false;
   modulo_eta = true
 }
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index daedd98921..b51da4fe08 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -845,6 +845,7 @@ let auto_unif_flags = {
   modulo_delta_types = full_transparent_state;
   resolve_evars = true;
   use_evars_pattern_unification = false;
+  modulo_betaiota = false;
   modulo_eta = true
 }
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 2831e5ec37..356752480f 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -79,6 +79,7 @@ let auto_unif_flags = {
   modulo_delta_types = full_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = true;
+  modulo_betaiota = true;
   modulo_eta = true
 }
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 40514a28fc..7dcd58d4eb 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -87,6 +87,7 @@ let rewrite_unif_flags = {
   Unification.modulo_delta_types = empty_transparent_state;
   Unification.resolve_evars = true;
   Unification.use_evars_pattern_unification = true;
+  Unification.modulo_betaiota = false;
   Unification.modulo_eta = true
 }
 
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index c633a9c0d5..334d653b12 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -301,6 +301,7 @@ let rewrite_unif_flags = {
   Unification.modulo_delta_types = full_transparent_state;
   Unification.resolve_evars = true;
   Unification.use_evars_pattern_unification = true;
+  Unification.modulo_betaiota = false;
   Unification.modulo_eta = true
 }
 
@@ -311,6 +312,7 @@ let rewrite2_unif_flags =
      Unification.modulo_delta_types = conv_transparent_state;
      Unification.resolve_evars = true;
      Unification.use_evars_pattern_unification = true;
+     Unification.modulo_betaiota = true;
      Unification.modulo_eta = true
   }
 
@@ -322,6 +324,7 @@ let general_rewrite_unif_flags () =
        Unification.modulo_delta_types = ts;
        Unification.resolve_evars = true;
        Unification.use_evars_pattern_unification = true;
+       Unification.modulo_betaiota = true;
        Unification.modulo_eta = true }
 
 let convertible env evd x y =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d960908337..f259dd9213 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -703,6 +703,7 @@ let elim_flags = {
   modulo_delta_types = full_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = true;
+  modulo_betaiota = false;
   modulo_eta = true
 }
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 8d7581179b..e70f65308d 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -283,36 +283,42 @@ let named_of_rel_context l =
 let string_of_global r =
  string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r)
 
-let rec declare_subclasses gr (rels, (tc, args)) =
-  let projs = list_map_filter 
-    (fun (n, b, proj) ->
-       if b then Option.map (fun p -> Nameops.out_name n, mkConst p) proj
-       else None) tc.cl_projs 
-  in
-  let instapp = appvectc (constr_of_global gr)
-    (Termops.extended_rel_vect 0 rels)
-  in
-  let projargs = 
-    Array.of_list (args @ [instapp])
-  in
-  let declare_proj (n, p) =
-    let ce = {
-      const_entry_body   = it_mkLambda_or_LetIn (mkApp (p, projargs)) rels;
-      const_entry_type   = None;
-      const_entry_opaque = false }
+let declare_subclasses gr cl =
+  let rec build_subclasses c (rels, (tc, args)) =
+    let projs = list_map_filter 
+      (fun (n, b, proj) ->
+	 if b then Option.map (fun p -> Nameops.out_name n, mkConst p) proj
+	 else None) tc.cl_projs 
     in
-    let cst = Declare.declare_constant ~internal:Declare.KernelSilent 
-      (Nameops.add_suffix (Nameops.add_suffix (id_of_string (string_of_global gr)) "_") 
-	 (string_of_id n))
-      (DefinitionEntry ce, IsAssumption Logical)
+    let instapp = appvectc (constr_of_global gr)
+      (Termops.extended_rel_vect 0 rels)
     in
-    let ty = Typeops.type_of_constant (Global.env ()) cst in
-      match class_of_constr ty with
-      | Some (rels, (tc, args) as cl) ->
-	  add_instance (Typeclasses.new_instance tc None false (ConstRef cst));
-	  declare_subclasses (ConstRef cst) cl
-      | None -> ()
-  in List.iter declare_proj projs
+    let projargs = 
+      Array.of_list (args @ [instapp])
+    in
+    let declare_proj (n, p) =
+      let body = it_mkLambda_or_LetIn (mkApp (p, projargs)) rels in
+	(*     let ce = { *)
+	(*       const_entry_body   = ; *)
+(*       const_entry_type   = None; *)
+(*       const_entry_opaque = false } *)
+(*     in *)
+(*     let cst = Declare.declare_constant ~internal:Declare.KernelSilent  *)
+(*       (Nameops.add_suffix (Nameops.add_suffix (id_of_string (string_of_global gr)) "_")  *)
+(* 	 (string_of_id n)) *)
+(*       (DefinitionEntry ce, IsAssumption Logical) *)
+(*     in *)
+      let ty = Retyping.get_type_of (Global.env ()) Evd.empty body in
+	match class_of_constr ty with
+	| Some (rels, (tc, args) as cl) ->
+	    (* 	  add_instance (Typeclasses.new_instance tc None false (ConstRef cst)); *)
+	    body :: build_subclasses body cl
+	| None -> []
+    in list_map_append declare_proj projs
+  in
+  let hints = build_subclasses (constr_of_global gr) cl in
+  let entry = List.map (fun c -> (None, false, None, c)) hints in
+    Auto.add_hints true (* local *) [typeclasses_db] (Auto.HintsResolveEntry entry)
 
 let context l =
   let env = Global.env() in