Merge PR#417: No cast surgery in let in

5 files changed, 25 insertions, 20 deletions

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 0cbb29575..49bafadc8 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -72,7 +72,7 @@ and constr_expr =
   | CCoFix of Loc.t * Id.t located * cofix_expr list
   | CProdN of Loc.t * binder_expr list * constr_expr
   | CLambdaN of Loc.t * binder_expr list * constr_expr
-  | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr
+  | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr option * constr_expr
   | CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * constr_expr list
   | CApp of Loc.t * (proj_flag * constr_expr) *
       (constr_expr * explicitation located option) list
@@ -111,10 +111,10 @@ and binder_expr =
 
 and fix_expr =
     Id.t located * (Id.t located option * recursion_order_expr) *
-      local_binder list * constr_expr * constr_expr
+      local_binder_expr list * constr_expr * constr_expr
 
 and cofix_expr =
-    Id.t located * local_binder list * constr_expr * constr_expr
+    Id.t located * local_binder_expr list * constr_expr * constr_expr
 
 and recursion_order_expr =
   | CStructRec
@@ -122,15 +122,15 @@ and recursion_order_expr =
   | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
 
 (** Anonymous defs allowed ?? *)
-and local_binder =
-  | LocalRawDef of Name.t located * constr_expr
-  | LocalRawAssum of Name.t located list * binder_kind * constr_expr
-  | LocalPattern of Loc.t * cases_pattern_expr * constr_expr option
+and local_binder_expr =
+  | CLocalAssum of Name.t located list * binder_kind * constr_expr
+  | CLocalDef of Name.t located * constr_expr * constr_expr option
+  | CLocalPattern of Loc.t * cases_pattern_expr * constr_expr option
 
 and constr_notation_substitution =
     constr_expr list *      (** for constr subterms *)
     constr_expr list list * (** for recursive notations *)
-    local_binder list list (** for binders subexpressions *)
+    local_binder_expr list list (** for binders subexpressions *)
 
 type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr
 
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index b3159c860..ced5a8b44 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -42,7 +42,7 @@ type glob_constr =
   | GApp of Loc.t * glob_constr * glob_constr list
   | GLambda of Loc.t * Name.t * binding_kind *  glob_constr * glob_constr
   | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr
-  | GLetIn of Loc.t * Name.t * glob_constr * glob_constr
+  | GLetIn of Loc.t * Name.t * glob_constr * glob_constr option * glob_constr
   | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses
       (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *)
   | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) *
@@ -78,6 +78,11 @@ and cases_clause = (Loc.t * Id.t list * cases_pattern list * glob_constr)
     of [t] are members of [il]. *)
 and cases_clauses = cases_clause list
 
+type extended_glob_local_binder =
+  | GLocalAssum of Loc.t * Name.t * binding_kind * glob_constr
+  | GLocalDef of Loc.t * Name.t * binding_kind * glob_constr * glob_constr option
+  | GLocalPattern of Loc.t * (cases_pattern * Id.t list) * Id.t * binding_kind * glob_constr
+
 (** A globalised term together with a closure representing the value
     of its free variables. Intended for use when these variables are taken
     from the Ltac environment. *)
diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index 1ab9980a5..753fa657a 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -30,7 +30,7 @@ type notation_constr =
   | NLambda of Name.t * notation_constr * notation_constr
   | NProd of Name.t * notation_constr * notation_constr
   | NBinderList of Id.t * Id.t * notation_constr * notation_constr
-  | NLetIn of Name.t * notation_constr * notation_constr
+  | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr
   | NCases of case_style * notation_constr option *
       (notation_constr * (Name.t * (inductive * Name.t list) option)) list *
       (cases_pattern list * notation_constr) list
diff --git a/intf/pattern.mli b/intf/pattern.mli
index 329ae837e..a32e7e4b9 100644
--- a/intf/pattern.mli
+++ b/intf/pattern.mli
@@ -68,7 +68,7 @@ type constr_pattern =
   | PProj of projection * constr_pattern
   | PLambda of Name.t * constr_pattern * constr_pattern
   | PProd of Name.t * constr_pattern * constr_pattern
-  | PLetIn of Name.t * constr_pattern * constr_pattern
+  | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern
   | PSort of glob_sort
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index f782dd639..25d3c705f 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -175,15 +175,15 @@ type plident = lident * lident list option
 type sort_expr = glob_sort
 
 type definition_expr =
-  | ProveBody of local_binder list * constr_expr
-  | DefineBody of local_binder list * Genredexpr.raw_red_expr option * constr_expr
+  | ProveBody of local_binder_expr list * constr_expr
+  | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr
       * constr_expr option
 
 type fixpoint_expr =
-    plident * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option
+    plident * (Id.t located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option
 
 type cofixpoint_expr =
-    plident * local_binder list * constr_expr * constr_expr option
+    plident * local_binder_expr list * constr_expr * constr_expr option
 
 type local_decl_expr =
   | AssumExpr of lname * constr_expr
@@ -202,14 +202,14 @@ type constructor_list_or_record_decl_expr =
   | Constructors of constructor_expr list
   | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list
 type inductive_expr =
-  plident with_coercion * local_binder list * constr_expr option * inductive_kind *
+  plident with_coercion * local_binder_expr list * constr_expr option * inductive_kind *
     constructor_list_or_record_decl_expr
 
 type one_inductive_expr =
-  plident * local_binder list * constr_expr option * constructor_expr list
+  plident * local_binder_expr list * constr_expr option * constructor_expr list
 
 type proof_expr =
-  plident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)
+  plident option * (local_binder_expr list * constr_expr * (lident option * recursion_order_expr) option)
 
 type syntax_modifier =
   | SetItemLevel of string list * Extend.production_level
@@ -365,12 +365,12 @@ type vernac_expr =
   (* Type classes *)
   | VernacInstance of
       bool * (* abstract instance *)
-      local_binder list * (* super *)
+      local_binder_expr list * (* super *)
 	typeclass_constraint * (* instance name, class name, params *)
 	(bool * constr_expr) option * (* props *)
 	hint_info_expr
 
-  | VernacContext of local_binder list
+  | VernacContext of local_binder_expr list
 
   | VernacDeclareInstances of
     (reference * hint_info_expr) list (* instances names, priorities and patterns *)