Generalized implementation of generalization.

- New constr_expr construct [CGeneralization of loc * binding_kind *
abstraction_kind option * constr_expr] to generalize the free vars of
the [constr_expr], binding these using [binding_kind] and making
a lambda or a pi (or deciding from the scope) using [abstraction_kind
option] (abstraction_kind = AbsLambda | AbsPi)
- Concrete syntax "`( a = 0 )" for explicit binding of [a] and "`{
... }" for implicit bindings (both "..(" and "_(" seem much more
difficult to implement). Subject to discussion! A few examples added
in a test-suite file.
- Also add missing syntax for implicit/explicit combinations for
_binders_: "{( )}" means implicit for the generalized (outer) vars,
explicit for the (inner) variable itself. Subject to discussion as well :)
- Factor much typeclass instance declaration code. We now just have to
force generalization of the term after the : in instance declarations.
One more step to using Instance for records.


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

1 files changed, 2 insertions, 5 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 662f2ac589..1ae1196a3d 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -1243,9 +1243,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 
-    ~on_free_vars:Classes.fail_on_free_vars
-    None
+  new_instance binders instance fields ~generalize:false None
 
 let require_library dirpath =
   let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in
@@ -1524,8 +1522,7 @@ let add_morphism binders m s n =
   in	  
   let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
     ignore(new_instance binders instance []
-	      ~on_free_vars:Classes.fail_on_free_vars
-	      ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst))
+	      ~generalize:false ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst))
 	      None)
 
 VERNAC COMMAND EXTEND AddSetoid1