Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)

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

3 files changed, 10 insertions, 12 deletions

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index b6dac63a98..55fce41aaa 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -310,10 +310,10 @@ let explain_unsolvable_implicit env = function
   | QuestionMark -> str "Cannot infer a term for this placeholder"
   | CasesType ->
       str "Cannot infer the type of this pattern-matching problem"
-  | AbstractionType (Name id) ->
+  | BinderType (Name id) ->
       str "Cannot infer a type for " ++ Nameops.pr_id id
-  | AbstractionType Anonymous ->
-      str "Cannot infer a type of this anonymous abstraction"
+  | BinderType Anonymous ->
+      str "Cannot infer a type of this anonymous binder"
   | ImplicitArg (c,n) ->
       str "Cannot infer the " ++ pr_ord n ++
       str " implicit argument of " ++ Nametab.pr_global_env Idset.empty c
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1cf01bf11b..cb1f21149f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -470,7 +470,6 @@ let vernac_define_module id binders_ast mty_ast_o mexpr_ast_o =
 (*     | true, _, _, _ -> *)
 (* 	error "Module definition not allowed in a Module Type" *)
 
-
 let vernac_end_module id =
   Declaremods.end_module id;
   if_verbose message 
@@ -714,6 +713,11 @@ let vernac_declare_implicits locqid = function
   | Some imps -> Impargs.declare_manual_implicits (Nametab.global locqid) imps
   | None -> Impargs.declare_implicits (Nametab.global locqid)
 
+let vernac_reserve idl c =
+  let t = Constrintern.interp_type Evd.empty (Global.env()) c in
+  let t = Detyping.detype (Global.env()) [] [] t in
+  List.iter (fun id -> Reserve.declare_reserved_type id t) idl
+
 let make_silent_if_not_pcoq b =
   if !pcoq <> None then 
     error "Turning on/off silent flag is not supported in Centaur mode"
@@ -791,14 +795,6 @@ let _ =
       optread=Pp_control.get_depth_boxes;
       optwrite=Pp_control.set_depth_boxes }
 
-let _ =
-  declare_int_option
-    { optsync=true;
-      optkey=SecondaryTable("Printing","Width");
-      optname="the printing width";
-      optread=Pp_control.get_margin;
-      optwrite=Pp_control.set_margin}
-
 let vernac_set_opacity opaq locqid =
   match Nametab.global locqid with
     | ConstRef sp ->
@@ -1202,6 +1198,7 @@ let interp c = match c with
   | VernacHintDestruct (id,l,p,n,tac) -> Dhyp.add_destructor_hint id l p n tac
   | VernacSyntacticDefinition (id,c,n) -> vernac_syntactic_definition id c n
   | VernacDeclareImplicits (qid,l) -> vernac_declare_implicits qid l
+  | VernacReserve (idl,c) -> vernac_reserve idl c
   | VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl
   | VernacSetOption (key,v) -> vernac_set_option key v
   | VernacUnsetOption key -> vernac_unset_option key
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 14c9a295e5..c332e894ad 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -228,6 +228,7 @@ type vernac_expr =
       identifier * (bool,unit) location * constr_expr * int * raw_tactic_expr
   | VernacSyntacticDefinition of identifier * constr_expr * int option
   | VernacDeclareImplicits of reference * int list option
+  | VernacReserve of identifier list * constr_expr
   | VernacSetOpacity of opacity_flag * reference list
   | VernacUnsetOption of Goptions.option_name
   | VernacSetOption of Goptions.option_name * option_value