From d91a0c27402f0f19a30147bb9d87387ca2a91fd0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 10:18:48 +0100
Subject: "Standardizing" the name LocalPatten into LocalRawPattern.

---
 vernac/command.ml | 2 +-
 vernac/record.ml  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index 4b4f4d2711..264f5f3369 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -563,7 +563,7 @@ let check_param = function
 | LocalRawDef (na, _) -> check_named na
 | LocalRawAssum (nas, Default _, _) -> List.iter check_named nas
 | LocalRawAssum (nas, Generalized _, _) -> ()
-| LocalPattern _ -> assert false
+| LocalRawPattern _ -> assert false
 
 let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   check_all_names_different indl;
diff --git a/vernac/record.ml b/vernac/record.ml
index b494430c28..05301b3dfc 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -110,7 +110,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
       List.iter 
 	(function LocalRawDef (b, _) -> error default_binder_kind b
 	   | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls
-           | LocalPattern (loc,_,_) ->
+           | LocalRawPattern (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
-- 
cgit v1.2.3


From 4e4fb7bd42364fd623f8e0e0d3007cd79d78764b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 18:21:51 +0100
Subject: Renaming local_binder into local_binder_expr.

This is a bit long, but it is to keep a symmetry with constr_expr.
---
 vernac/classes.mli |  4 ++--
 vernac/command.ml  |  4 ++--
 vernac/command.mli | 10 +++++-----
 vernac/record.mli  |  2 +-
 4 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'vernac')

diff --git a/vernac/classes.mli b/vernac/classes.mli
index d2cb788eae..69ea841582 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 264f5f3369..edd2401c7c 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -370,7 +370,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."
@@ -830,7 +830,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 616afb91f0..bccc22ae92 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.mli b/vernac/record.mli
index c50e577860..3fd651db90 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
 
-- 
cgit v1.2.3


From 648ce5e08f7245f2a775abd1304783c4167e9f2e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 18:24:58 +0100
Subject: Unifying standard "constr_level" names for constructors of
 local_binder_expr.

RawLocal -> CLocal
---
 vernac/command.ml | 8 ++++----
 vernac/record.ml  | 6 +++---
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index edd2401c7c..cdc1c88e63 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -560,10 +560,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 _, _) -> ()
-| LocalRawPattern _ -> 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;
diff --git a/vernac/record.ml b/vernac/record.ml
index 05301b3dfc..a6c8f8b369 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -108,9 +108,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
-           | LocalRawPattern (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
-- 
cgit v1.2.3


From f9a4ca41bc1313300f5f9b9092fe24825f435706 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 1 Feb 2017 15:56:45 +0100
Subject: Replacing "cast surgery" in LetIn by a proper field (see PR #404).

This is a patch fulfilling the relevant remark of Maxime that an
explicit information at the ML type level would be better than "cast
surgery" to carry the optional type of a let-in.

There are a very few semantic changes.
- a "(x:t:=c)" in a block of binders is now written in the more
  standard way "(x:=c:t)"
- in notations, the type of a let-in is not displayed if not
  explicitly asked so.

See discussion at PR #417 for more information.
---
 vernac/command.ml | 6 +++---
 vernac/record.ml  | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index cdc1c88e63..8244ee5346 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
@@ -416,7 +416,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
@@ -560,7 +560,7 @@ let check_named (loc, na) = match na with
 
 
 let check_param = function
-| CLocalDef (na, _) -> check_named na
+| CLocalDef (na, _, _) -> check_named na
 | CLocalAssum (nas, Default _, _) -> List.iter check_named nas
 | CLocalAssum (nas, Generalized _, _) -> ()
 | CLocalPattern _ -> assert false
diff --git a/vernac/record.ml b/vernac/record.ml
index a6c8f8b369..51d89f1551 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -108,7 +108,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
       | _ -> ()
     in
       List.iter 
-	(function CLocalDef (b, _) -> error default_binder_kind b
+	(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
-- 
cgit v1.2.3


From 43ac25fd5218fb92b3971c8df8be4f38894e27f3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 22 Mar 2017 23:23:14 +0100
Subject: [nit] Fix a couple incorrect uses of msg_error.

---
 vernac/vernacentries.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 32e18a0149..f179084004 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. *)
-- 
cgit v1.2.3


From 584a832d4f681d34c7cbdd87d9ceb7a742b39959 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 22 Feb 2017 00:23:10 +0100
Subject: [stm] Remove some obsolete vernacs/classification.

This is the good parts of PR #360.

IIUC, these vernacular were meant mostly for debugging and they are
not supposed to be of any use these days.

Back and join are still there not to break the testing infrastructure,
but some day they should go away.
---
 vernac/vernacentries.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 32e18a0149..64c06d77a2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2210,6 +2210,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 -> 
@@ -2218,9 +2223,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) ->
-- 
cgit v1.2.3