- Improve [Context] vernacular to allow arbitrary binders, not just

classes, and simplify the implementation.
- Experimental syntax {{ cl : Class args }} and (( cl : Class args ))
which respectively make cl an implicit or explicit argument ({{ }} is
equivalent to [ ]). Could be extended to any type of binder, eg. 
[Definition flip ((R : relation carrier)) : relation carrier := ...].
The idea behind double brackets is to distinguish macro-binders which 
perform implicit generalization from regular binders. It could also save
[ ] for other uses.
- Fix bug #1901 about {} binders in records.


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

5 files changed, 54 insertions, 32 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 5599f4d66..1837bca9a 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -191,7 +191,7 @@ let new_class id par ar sup props =
     (* Make the class and all params implicits in the projections *)
     let ctx_impls = implicits_of_context ctx_params in
     let len = succ (List.length ctx_params) in
-      List.rev_map (fun x -> ctx_impls @ Impargs.lift_implicits len x) prop_impls
+      List.map (fun x -> ctx_impls @ Impargs.lift_implicits len x) prop_impls
   in
   let impl, projs = 
     let params = ctx_params and fields = ctx_props in
@@ -261,13 +261,26 @@ let binders_of_lidents l =
   List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Implicit, CHole (loc, None))) l
 
 let type_ctx_instance isevars env ctx inst subst =
-  List.fold_left2
-    (fun (subst, instctx) (na, _, t) ce ->
-      let t' = substl subst t in
-      let c = interp_casted_constr_evars isevars env ce t' in
-      let d = na, Some c, t' in
-	c :: subst, d :: instctx)
-    (subst, []) (List.rev ctx) inst
+  let (s, _) = 
+    List.fold_left2
+      (fun (subst, instctx) (na, _, t) ce ->
+	let t' = substl subst t in
+	let c = interp_casted_constr_evars isevars env ce t' in
+	let d = na, Some c, t' in
+	  c :: subst, d :: instctx)
+      (subst, []) (List.rev ctx) inst
+  in s
+
+(* let type_ctx_instance isevars env ctx inst subst = *)
+(*   let (s, _, _) =  *)
+(*     List.fold_left2 *)
+(*       (fun (s, env, n) (na, _, t) ce -> *)
+(* 	let t' = substnl subst n t in *)
+(* 	let c = interp_casted_constr_evars isevars env ce t' in *)
+(* 	let d = na, Some c, t' in *)
+(* 	  (substl s c :: s, push_rel d env, succ n)) *)
+(*       ([], env, 0) (List.rev ctx) inst *)
+(*   in s @ subst *)
 
 let refine_ref = ref (fun _ -> assert(false))
 
@@ -397,7 +410,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
       end
     else
       begin
-	let subst, _propsctx = 
+	let subst = 
 	  let props = 
 	    List.map (fun (x, l, d) -> 
 	      x, Topconstr.abstract_constr_expr d (binders_of_lidents l))
@@ -449,21 +462,26 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 	  end
       end
 
+let named_of_rel_context l =
+  let acc, ctx = 
+    List.fold_right 
+      (fun (na, b, t) (subst, ctx) ->
+	let id = match na with Anonymous -> raise (Invalid_argument "named_of_rel_context") | Name id -> id in
+	let d = (id, Option.map (substl subst) b, substl subst t) in
+	  (mkVar id :: subst, d :: ctx))
+      l ([], [])
+  in ctx
+
 let context ?(hook=fun _ -> ()) l =
   let env = Global.env() in
-  let isevars = ref (Evd.create_evar_defs Evd.empty) in
-  let avoid = Termops.ids_of_context env in
-  let ctx, l = 
-    List.fold_left 
-      (fun (ids, acc) x ->
-	let ids, ctx, cstr = Implicit_quantifiers.generalize_class_binder_raw ids x in
-	  (ids, (cstr :: ctx) @ acc))
-      (vars_of_env env, []) l
+  let evars = ref (Evd.create_evar_defs Evd.empty) in
+  let (env', fullctx), impls = interp_context_evars evars env l in
+  let fullctx = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) fullctx in
+  let ce t = Evarutil.check_evars env Evd.empty !evars t in
+  List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx;
+  let ctx = try named_of_rel_context fullctx with _ -> 
+    error "Anonymous variables not allowed in contexts"
   in
-  let env', avoid, l = interp_typeclass_context_evars isevars env avoid (List.rev l) in
-  isevars := Evarutil.nf_evar_defs !isevars;
-  let sigma = Evd.evars_of !isevars in
-  let fullctx = Evarutil.nf_named_context_evar sigma l in
     List.iter (function (id,_,t) -> 
       if Lib.is_modtype () then 
 	let cst = Declare.declare_internal_constant id
@@ -480,4 +498,4 @@ let context ?(hook=fun _ -> ()) l =
 	 match class_of_constr t with
 	     None -> ()
 	   | Some tc -> hook (VarRef id)))
-      (List.rev fullctx)
+      (List.rev ctx)
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index c10ee4c97..970f3e2ab 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -86,8 +86,7 @@ val id_of_class : typeclass -> identifier
 (* Context command *)    
 
 val context : ?hook:(Libnames.global_reference -> unit) -> 
-  (Names.name Util.located * (Rawterm.binding_kind * Rawterm.binding_kind) *
-  Topconstr.constr_expr) list -> unit
+  local_binder list -> unit
 
 (* Forward ref for refine *)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 14e64ead4..c3bddf1d9 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -556,12 +556,18 @@ let interp_mutual paramsl indl notations finite =
     mind_entry_consnames = cnames;
     mind_entry_lc = ctypes
   }) indl arities constructors in
-
+  let impls = 
+    let len = List.length ctx_params in
+      List.map (fun (_,_,impls) ->
+	userimpls, List.map (fun impls -> 
+	  userimpls @ (lift_implicits len impls)) impls) constructors
+  in
   (* Build the mutual inductive entry *)
   { mind_entry_params = List.map prepare_param ctx_params;
     mind_entry_record = false; 
     mind_entry_finite = finite; 
-    mind_entry_inds = entries }, (List.map (fun (_,_,impls) -> userimpls, impls) constructors)
+    mind_entry_inds = entries }, 
+    impls
 
 let eq_constr_expr c1 c2 =
   try let _ = Constrextern.check_same_type c1 c2 in true with _ -> false
@@ -615,14 +621,15 @@ let _ =
 
 let declare_mutual_with_eliminations isrecord mie impls =
   let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
-  let params = List.length mie.mind_entry_params in
   let (_,kn) = declare_mind isrecord mie in    
     list_iter_i (fun i (indimpls, constrimpls) -> 
       let ind = (kn,i) in
+	maybe_declare_manual_implicits false (IndRef ind)
+	  (is_implicit_args()) indimpls;
 	list_iter_i
 	  (fun j impls -> 
 	    maybe_declare_manual_implicits false (ConstructRef (ind, succ j))
-	      (is_implicit_args()) (indimpls @ (lift_implicits params impls)))
+	      (is_implicit_args()) impls)
 	  constrimpls)
       impls;
     if_verbose ppnl (minductive_message names);
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7ccfe526d..c882d2108 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -602,7 +602,7 @@ let vernac_instance glob sup inst props pri =
   ignore(Classes.new_instance ~global:glob sup inst props pri)
 
 let vernac_context l =
-  if !Flags.dump then List.iter (fun x -> Dumpglob.dump_constraint x true "var") l;
+  if !Flags.dump then List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l;
   Classes.context l
 
 let vernac_declare_instance id =
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 2c646f6bc..e1b316481 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -239,9 +239,7 @@ type vernac_expr =
 	(lident * lident list * constr_expr) list * (* props *)
 	int option (* Priority *)
 
-  | VernacContext of 
-      (Names.name Util.located * (Rawterm.binding_kind * Rawterm.binding_kind) *
-	  Topconstr.constr_expr) list
+  | VernacContext of local_binder list
 	
   | VernacDeclareInstance of
       lident (* instance name *)