Merge branch 'trunk' into pr379

7 files changed, 26 insertions, 25 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index c3300a361..833719965 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -338,7 +338,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
                      the refinement manually.*)
 		let gls = List.rev (Evd.future_goals evm) in
                 let evm = Evd.reset_future_goals evm in
-                Lemmas.start_proof id kind evm (EConstr.of_constr termtype)
+                Lemmas.start_proof id ?pl kind evm (EConstr.of_constr termtype)
 		(Lemmas.mk_hook
                   (fun _ -> instance_hook k pri global imps ?hook));
                  (* spiwack: I don't know what to do with the status here. *)
diff --git a/vernac/classes.mli b/vernac/classes.mli
index d2cb788ea..69ea84158 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -42,7 +42,7 @@ val new_instance :
   ?global:bool -> (** Not global by default. *)
   ?refine:bool -> (** Allow refinement *)
   Decl_kinds.polymorphic ->
-  local_binder list ->
+  local_binder_expr list ->
   typeclass_constraint ->
   (bool * constr_expr) option ->
   ?generalize:bool ->
@@ -63,4 +63,4 @@ val id_of_class : typeclass -> Id.t
 
 (** returns [false] if, for lack of section, it declares an assumption
     (unless in a module type). *)
-val context : Decl_kinds.polymorphic -> local_binder list -> bool
+val context : Decl_kinds.polymorphic -> local_binder_expr list -> bool
diff --git a/vernac/command.ml b/vernac/command.ml
index db203b425..0393669d4 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -55,7 +55,7 @@ let rec under_binders env sigma f n c =
 
 let rec complete_conclusion a cs = function
   | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c)
-  | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c)
+  | CLetIn (loc,na,b,t,c) -> CLetIn (loc,na,b,t,complete_conclusion a cs c)
   | CHole (loc, k, _, _) ->
       let (has_no_args,name,params) = a in
       if not has_no_args then
@@ -378,7 +378,7 @@ type structured_one_inductive_expr = {
 }
 
 type structured_inductive_expr =
-  local_binder list * structured_one_inductive_expr list
+  local_binder_expr list * structured_one_inductive_expr list
 
 let minductive_message warn = function
   | []  -> error "No inductive definition."
@@ -424,7 +424,7 @@ let rec check_anonymous_type ind =
     match ind with
     | GSort (_, GType []) -> true
     | GProd (_, _, _, _, e) 
-    | GLetIn (_, _, _, e)
+    | GLetIn (_, _, _, _, e)
     | GLambda (_, _, _, _, e)
     | GApp (_, e, _)
     | GCast (_, e, _) -> check_anonymous_type e
@@ -569,10 +569,10 @@ let check_named (loc, na) = match na with
 
 
 let check_param = function
-| LocalRawDef (na, _) -> check_named na
-| LocalRawAssum (nas, Default _, _) -> List.iter check_named nas
-| LocalRawAssum (nas, Generalized _, _) -> ()
-| LocalPattern _ -> assert false
+| CLocalDef (na, _, _) -> check_named na
+| CLocalAssum (nas, Default _, _) -> List.iter check_named nas
+| CLocalAssum (nas, Generalized _, _) -> ()
+| CLocalPattern _ -> assert false
 
 let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   check_all_names_different indl;
@@ -840,7 +840,7 @@ type structured_fixpoint_expr = {
   fix_name : Id.t;
   fix_univs : lident list option;
   fix_annot : Id.t Loc.located option;
-  fix_binders : local_binder list;
+  fix_binders : local_binder_expr list;
   fix_body : constr_expr option;
   fix_type : constr_expr
 }
diff --git a/vernac/command.mli b/vernac/command.mli
index fae783ef0..7cd0afeec 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -32,7 +32,7 @@ val get_declare_definition_hook : unit -> (Safe_typing.private_constants definit
 (** {6 Definitions/Let} *)
 
 val interp_definition :
-  lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr ->
+  lident list option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
   constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * 
       Universes.universe_binders * Impargs.manual_implicits
 
@@ -41,13 +41,13 @@ val declare_definition : Id.t -> definition_kind ->
     Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
 
 val do_definition : Id.t -> definition_kind -> lident list option ->
-  local_binder list -> red_expr option -> constr_expr ->
+  local_binder_expr list -> red_expr option -> constr_expr ->
   constr_expr option -> unit Lemmas.declaration_hook -> unit
 
 (** {6 Parameters/Assumptions} *)
 
 (* val interp_assumption : env -> evar_map ref -> *)
-(*   local_binder list -> constr_expr ->  *)
+(*   local_binder_expr list -> constr_expr ->  *)
 (*   types Univ.in_universe_context_set * Impargs.manual_implicits *)
 
 (** returns [false] if the assumption is neither local to a section,
@@ -78,7 +78,7 @@ type structured_one_inductive_expr = {
 }
 
 type structured_inductive_expr =
-  local_binder list * structured_one_inductive_expr list
+  local_binder_expr list * structured_one_inductive_expr list
 
 val extract_mutual_inductive_declaration_components :
   (one_inductive_expr * decl_notation list) list ->
@@ -114,7 +114,7 @@ type structured_fixpoint_expr = {
   fix_name : Id.t;
   fix_univs : lident list option;
   fix_annot : Id.t Loc.located option;
-  fix_binders : local_binder list;
+  fix_binders : local_binder_expr list;
   fix_body : constr_expr option;
   fix_type : constr_expr
 }
diff --git a/vernac/record.ml b/vernac/record.ml
index e1c99fa2a..490a2a49d 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -109,9 +109,9 @@ let typecheck_params_and_fields def id pl t ps nots fs =
       | _ -> ()
     in
       List.iter 
-	(function LocalRawDef (b, _) -> error default_binder_kind b
-	   | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls
-           | LocalPattern (loc,_,_) ->
+	(function CLocalDef (b, _, _) -> error default_binder_kind b
+	   | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls
+           | CLocalPattern (loc,_,_) ->
               Loc.raise ~loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps
   in 
   let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in
diff --git a/vernac/record.mli b/vernac/record.mli
index c50e57786..3fd651db9 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -39,7 +39,7 @@ val declare_structure :
 
 val definition_structure :
   inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind *
-  plident with_coercion * local_binder list *
+  plident with_coercion * local_binder_expr list *
   (local_decl_expr with_instance with_priority with_notation) list *
   Id.t * constr_expr option -> global_reference
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 66796d1dc..53d49ddbc 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -67,8 +67,7 @@ let show_node () =
       could, possibly, be cleaned away. (Feb. 2010) *)
   ()
 
-let show_thesis () =
-     Feedback.msg_error (anomaly (Pp.str "TODO") )
+let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO")
 
 let show_top_evars () =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
@@ -2216,6 +2215,11 @@ let with_fail b f =
 let interp ?(verbosely=true) ?proof (loc,c) =
   let orig_program_mode = Flags.is_program_mode () in
   let rec aux ?locality ?polymorphism isprogcmd = function
+
+    (* This assert case will be removed when fake_ide can understand
+       completion feedback *)
+    | VernacStm _ -> assert false (* Done by Stm *)
+
     | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c
     | VernacProgram _ -> CErrors.error "Program mode specified twice"
     | VernacLocal (b, c) when Option.is_empty locality -> 
@@ -2224,9 +2228,6 @@ let interp ?(verbosely=true) ?proof (loc,c) =
       aux ?locality ~polymorphism:b isprogcmd c
     | VernacPolymorphic (b, c) -> CErrors.error "Polymorphism specified twice"
     | VernacLocal _ -> CErrors.error "Locality specified twice"
-    | VernacStm (Command c) -> aux ?locality ?polymorphism isprogcmd c
-    | VernacStm (PGLast c) -> aux ?locality ?polymorphism isprogcmd c
-    | VernacStm _ -> assert false (* Done by Stm *)
     | VernacFail v ->
         with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v)
     | VernacTimeout (n,v) ->