More factorization of inductive/record and typeclasses: move class

declaration code to toplevel/record, including support for singleton
classes as definitions. Parsing code also factorized. Arnaud: one more
thing to think about when refactoring the definitions in vernacentries.
Add support for specifying what to do with anonymous variables in
contexts during internalisation (fixes bug #1982), current choice is to
generate a name for typeclass bindings.


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

1 files changed, 17 insertions, 15 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index e051d1aad..33bc17624 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -71,6 +71,8 @@ let e_give_exact flags c gl =
     if occur_existential t1 or occur_existential t2 then 
       tclTHEN (Clenvtac.unify (* ~flags *) t1) (exact_check c) gl
     else exact_check c gl
+(*   let t1 = (pf_type_of gl c) in *)
+(*     tclTHEN (Clenvtac.unify ~flags t1) (exact_check c) gl *)
       
 let assumption flags id = e_give_exact flags (mkVar id)
 
@@ -1242,7 +1244,7 @@ let declare_an_instance n s args =
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance binders instance fields = 
-  new_instance binders instance fields ~generalize:false None
+  new_instance binders instance (CRecord (dummy_loc,None,fields)) ~generalize:false None
 
 let require_library dirpath =
   let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in
@@ -1251,17 +1253,17 @@ let require_library dirpath =
 let declare_instance_refl binders a aeq n lemma = 
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" 
   in anew_instance binders instance 
-       [((dummy_loc,id_of_string "reflexivity"),[],lemma)]
+       [((dummy_loc,id_of_string "reflexivity"),lemma)]
 
 let declare_instance_sym binders a aeq n lemma = 
   let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
   in anew_instance binders instance 
-       [((dummy_loc,id_of_string "symmetry"),[],lemma)]
+       [((dummy_loc,id_of_string "symmetry"),lemma)]
 
 let declare_instance_trans binders a aeq n lemma = 
   let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive" 
   in anew_instance binders instance 
-       [((dummy_loc,id_of_string "transitivity"),[],lemma)]
+       [((dummy_loc,id_of_string "transitivity"),lemma)]
 
 let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor (false,None)))
 
@@ -1286,16 +1288,16 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" 
 	in ignore(
 	    anew_instance binders instance 
-	      [((dummy_loc,id_of_string "PreOrder_Reflexive"), [], lemma1);
-	       ((dummy_loc,id_of_string "PreOrder_Transitive"),[], lemma3)])
+	      [((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 instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" 
 	in ignore(
 	    anew_instance binders instance 
-	      [((dummy_loc,id_of_string "PER_Symmetric"), [], lemma2);
-	       ((dummy_loc,id_of_string "PER_Transitive"),[], lemma3)])
+	      [((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
@@ -1303,9 +1305,9 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" 
 	in ignore(
 	  anew_instance binders instance 
-	    [((dummy_loc,id_of_string "Equivalence_Reflexive"), [], lemma1);
-	     ((dummy_loc,id_of_string "Equivalence_Symmetric"),  [], lemma2);
-	     ((dummy_loc,id_of_string "Equivalence_Transitive"),[], lemma3)])
+	    [((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
 
@@ -1483,9 +1485,9 @@ let add_setoid binders a aeq t n =
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
   in ignore(
     anew_instance binders instance
-      [((dummy_loc,id_of_string "Equivalence_Reflexive"), [], mkappc "Seq_refl" [a;aeq;t]);
-       ((dummy_loc,id_of_string "Equivalence_Symmetric"),  [], mkappc "Seq_sym" [a;aeq;t]);
-       ((dummy_loc,id_of_string "Equivalence_Transitive"),[], mkappc "Seq_trans" [a;aeq;t])])
+      [((dummy_loc,id_of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
+       ((dummy_loc,id_of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
+       ((dummy_loc,id_of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
 
 let add_morphism_infer m n =
   init_setoid ();
@@ -1520,7 +1522,7 @@ let add_morphism binders m s n =
 	     [cHole; s; m]))
   in	  
   let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
-    ignore(new_instance binders instance []
+    ignore(new_instance binders instance (CRecord (dummy_loc,None,[]))
 	      ~generalize:false ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst))
 	      None)