Fixes w.r.t. let binders in class contexts and Add Parametric

Morphism/Relation bindings.


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

2 files changed, 25 insertions, 25 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index ad627c8418..97129a56b9 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -1236,31 +1236,31 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	ignore (declare_instance_refl binders a aeq n lemma1); 
 	ignore (declare_instance_sym binders a aeq n lemma2)
     | (Some lemma1, None, Some lemma3) -> 
-	let lemma_refl = declare_instance_refl binders a aeq n lemma1 in
-	let lemma_trans = declare_instance_trans binders a aeq n lemma3 in
+	let _lemma_refl = declare_instance_refl binders a aeq n lemma1 in
+	let _lemma_trans = declare_instance_trans binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" 
 	in ignore(
 	    anew_instance binders instance 
-	      [((dummy_loc,id_of_string "PreOrder_Reflexive"), [], mkIdentC lemma_refl);
-	       ((dummy_loc,id_of_string "PreOrder_Transitive"),[], mkIdentC lemma_trans)])
+	      [((dummy_loc,id_of_string "PreOrder_Reflexive"), [], lemma1);
+	       ((dummy_loc,id_of_string "PreOrder_Transitive"),[], lemma3)])
     | (None, Some lemma2, Some lemma3) -> 
-	let lemma_sym = declare_instance_sym binders a aeq n lemma2 in
-	let lemma_trans = declare_instance_trans binders a aeq n lemma3 in
+	let _lemma_sym = declare_instance_sym binders a aeq n lemma2 in
+	let _lemma_trans = declare_instance_trans binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" 
 	in ignore(
 	    anew_instance binders instance 
-	      [((dummy_loc,id_of_string "PER_Symmetric"),  [], mkIdentC lemma_sym);
-	       ((dummy_loc,id_of_string "PER_Transitive"),[], mkIdentC lemma_trans)])
+	      [((dummy_loc,id_of_string "PER_Symmetric"), [], lemma2);
+	       ((dummy_loc,id_of_string "PER_Transitive"),[], lemma3)])
      | (Some lemma1, Some lemma2, Some lemma3) -> 
-	let lemma_refl = declare_instance_refl binders a aeq n lemma1 in 
-	let lemma_sym = declare_instance_sym binders a aeq n lemma2 in
-	let lemma_trans = declare_instance_trans binders a aeq n lemma3 in
+	let _lemma_refl = declare_instance_refl binders a aeq n lemma1 in 
+	let _lemma_sym = declare_instance_sym binders a aeq n lemma2 in
+	let _lemma_trans = declare_instance_trans binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" 
 	in ignore(
 	  anew_instance binders instance 
-	    [((dummy_loc,id_of_string "Equivalence_Reflexive"), [], mkIdentC lemma_refl);
-	     ((dummy_loc,id_of_string "Equivalence_Symmetric"),  [], mkIdentC lemma_sym);
-	     ((dummy_loc,id_of_string "Equivalence_Transitive"),[], mkIdentC lemma_trans)])
+	    [((dummy_loc,id_of_string "Equivalence_Reflexive"), [], lemma1);
+	     ((dummy_loc,id_of_string "Equivalence_Symmetric"),  [], lemma2);
+	     ((dummy_loc,id_of_string "Equivalence_Transitive"),[], lemma3)])
 
 type 'a binders_let_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
 
@@ -1410,9 +1410,10 @@ let build_morphism_signature m =
   let morph = 
     mkApp (Lazy.force morphism_type, [| t; sig_; m |])
   in
-  let evd = resolve_all_evars_once false (true, default_eauto_depth) env
-    (fun x evi -> class_of_constr evi.Evd.evar_concl <> None) !isevars in
-    Evarutil.nf_isevar evd morph
+  let evd = 
+    Typeclasses.resolve_typeclasses ~fail:true ~onlyargs:false env !isevars in
+  let m = Evarutil.nf_isevar evd morph in
+    Evarutil.check_evars env Evd.empty evd m; m
 	
 let default_morphism sign m =
   let env = Global.env () in
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index db5c548553..8c34c32edd 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -235,6 +235,10 @@ let decompose_named_assum =
 	let decl = (na,None,substl subst t) in
 	let subst' = mkVar na :: subst in
 	  prodec_rec subst' (add_named_decl decl l) (substl subst' c)
+      | LetIn (Name na, b, t, c) ->
+	let decl = (na,Some (substl subst b),substl subst t) in
+	let subst' = mkVar na :: subst in
+	  prodec_rec subst' (add_named_decl decl l) (substl subst' c)
       | Cast (c,_,_)      -> prodec_rec subst l c
       | _               -> l,c
   in prodec_rec [] []
@@ -492,12 +496,12 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
   let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in
   let ctx, avoid = name_typeclass_binders bound ctx in
   let ctx = List.append ctx (List.rev gen_ctx) in
-  let k, ctx', subst = 
+  let k, ctx', imps, subst = 
     let c = Command.generalize_constr_expr tclass ctx in
-    let _imps, c' = interp_type_evars isevars env c in
+    let imps, c' = interp_type_evars isevars env c in
     let ctx, c = decompose_named_assum c' in
     let cl, args = Typeclasses.dest_class_app c in
-      cl, ctx, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
+      cl, ctx, imps, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
   in
   let id = 
     match snd instid with
@@ -515,11 +519,6 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
   isevars := resolve_typeclasses env !isevars;
   let sigma = Evd.evars_of !isevars in
   let substctx = Typeclasses.nf_substitution sigma subst in
-  let imps = 
-    Util.list_map_i 
-      (fun i (na, b, t) -> ExplByPos (i, Some na), (true, true))
-      1 ctx'
-  in
     if Lib.is_modtype () then
       begin
 	let _, ty_constr = instance_constructor k (List.rev_map snd substctx) in