- Add modulo_delta_types flag for unification to allow full

conversion when checking types of instanciations while having
restricted delta reduction for unification itself. This
makes auto/eauto... backward compatible.
- Change semantics of [Instance foo : C a.] to _not_ search
for an instance of [C a] automatically and potentially slow
down interaction, except for trivial classes with no fields.
Use [C a := _.] or [C a := {}] to search for an instance of
the class or for every field.
- Correct treatment of transparency information for classes 
declared in sections.


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

5 files changed, 30 insertions, 15 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index c5bcb631e..6e92d74ab 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -36,8 +36,6 @@ let flex_kind_of_term c l =
     | Meta _ | Case _ | Fix _ -> PseudoRigid c
     | Cast _ | App _ -> assert false
 
-let is_rigid = function Rigid _ -> true | _ -> false
-
 let eval_flexible_term ts env c =
   match kind_of_term c with
   | Const c -> 
@@ -200,7 +198,6 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
 and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
   (* Evar must be undefined since we have flushed evars *)
   match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with
-
     | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
 	let f1 i =
 	  if List.length l1 > List.length l2 then
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index cca7aee1d..eabef3641 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -32,10 +32,10 @@ let register_remove_instance_hint =
   (:=) remove_instance_hint_ref
 let remove_instance_hint id = !remove_instance_hint_ref id
 
-let set_typeclass_transparency_ref = ref (fun id pri -> assert false)
+let set_typeclass_transparency_ref = ref (fun id local c -> assert false)
 let register_set_typeclass_transparency =
   (:=) set_typeclass_transparency_ref
-let set_typeclass_transparency gr c = !set_typeclass_transparency_ref gr c
+let set_typeclass_transparency gr local c = !set_typeclass_transparency_ref gr local c
 
 type rels = constr list
 
@@ -200,7 +200,11 @@ let discharge_class (_,cl) =
       cl_props = props;
       cl_projs = list_smartmap (fun (x, y, z) -> x, y, Option.smartmap Lib.discharge_con z) cl.cl_projs }
 
-let rebuild_class cl = cl
+let rebuild_class cl = 
+  try 
+    let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in
+      set_typeclass_transparency cst false false; cl
+  with _ -> cl
 
 let class_input =
   declare_object
@@ -305,7 +309,7 @@ let add_constant_class cst =
       cl_projs = []
     }
   in add_class tc;
-    set_typeclass_transparency (EvalConstRef cst) false
+    set_typeclass_transparency (EvalConstRef cst) false false
       
 let add_inductive_class ind =
   let mind, oneind = Global.lookup_inductive ind in
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 1fe955b0c..77567bece 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -87,8 +87,8 @@ val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool ->
   env -> evar_map -> evar_map
 val resolve_one_typeclass : env -> evar_map -> types -> open_constr
 
-val register_set_typeclass_transparency : (evaluable_global_reference -> bool -> unit) -> unit
-val set_typeclass_transparency : evaluable_global_reference -> bool -> unit
+val register_set_typeclass_transparency : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) -> unit
+val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
 
 val register_add_instance_hint : (global_reference -> bool (* local? *) -> int option -> unit) -> unit
 val register_remove_instance_hint : (global_reference -> unit) -> unit
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5982de65e..7b01134e0 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -168,6 +168,7 @@ type unify_flags = {
   modulo_conv_on_closed_terms : Names.transparent_state option;
   use_metas_eagerly : bool;
   modulo_delta : Names.transparent_state;
+  modulo_delta_types : Names.transparent_state;
   resolve_evars : bool;
   use_evars_pattern_unification : bool;
   modulo_eta : bool
@@ -177,6 +178,7 @@ let default_unify_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = true;
   modulo_delta = full_transparent_state;
+  modulo_delta_types = full_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = true;
   modulo_eta = true
@@ -186,6 +188,7 @@ let default_no_delta_unify_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = true;
   modulo_delta = empty_transparent_state;
+  modulo_delta_types = full_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = false;
   modulo_eta = true
@@ -574,10 +577,12 @@ let applyHead env evd n c  =
   in
   apprec n c (Typing.type_of env evd c) evd
 
-let is_mimick_head f =
+let is_mimick_head ts f =
   match kind_of_term f with
-      (Const _|Var _|Rel _|Construct _|Ind _) -> true
-    | _ -> false
+  | Const c -> not (Closure.is_transparent_constant ts c)
+  | Var id -> not (Closure.is_transparent_variable ts id)
+  | (Rel _|Construct _|Ind _) -> true
+  | _ -> false
 
 let try_to_coerce env evd c cty tycon =
   let j = make_judge c cty in
@@ -663,18 +668,18 @@ let w_merge env with_types flags (evd,metas,evars) =
 	  | App (f,cl) when occur_meta rhs' ->
 	      if occur_evar evk rhs' then
                 error_occur_check curenv evd evk rhs';
-	      if is_mimick_head f then
+	      if is_mimick_head flags.modulo_delta f then
 		let evd' =
 		  mimick_undefined_evar evd flags f (Array.length cl) evk in
 		w_merge_rec evd' metas evars eqns
 	      else
 		let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in
-		w_merge_rec (solve_simple_evar_eqn flags.modulo_delta curenv evd' ev rhs'')
+		w_merge_rec (solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'')
 		  metas evars' eqns
 
           | _ ->
 	    let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in
-	      w_merge_rec (solve_simple_evar_eqn flags.modulo_delta curenv evd' ev rhs'')
+	      w_merge_rec (solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'')
 		metas evars' eqns
 	end
     | [] ->
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index cc3040a9e..0462688b4 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -14,6 +14,7 @@ type unify_flags = {
   modulo_conv_on_closed_terms : Names.transparent_state option;
   use_metas_eagerly : bool;
   modulo_delta : Names.transparent_state;
+  modulo_delta_types : Names.transparent_state;
   resolve_evars : bool;
   use_evars_pattern_unification : bool;
   modulo_eta : bool
@@ -49,3 +50,11 @@ val w_coerce_to_type : env -> evar_map -> constr -> types -> types ->
    (exported for inv.ml) *)
 val abstract_list_all :
   env -> evar_map -> constr -> constr -> constr list -> constr
+
+
+(* For tracing *)
+
+val w_merge : env -> bool -> unify_flags -> evar_map *
+  (metavariable * constr * (instance_constraint * instance_typing_status)) list *
+  (env * types pexistential * types) list -> evar_map
+