Merge branch 'trunk' into pr379

14 files changed, 125 insertions, 107 deletions

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 3aa572529..a29480a55 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -264,7 +264,7 @@ let prod_one_id (loc,id) glob =
 	 GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob)
 
 let let_in_one_alias (id,pat) glob =
-  GLetIn (Loc.ghost,Name id, glob_of_pat pat, glob)
+  GLetIn (Loc.ghost,Name id, glob_of_pat pat, None, glob)
 
 let rec bind_primary_aliases map pat =
   match pat with
@@ -359,10 +359,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
     let rids=ref ([],pat_vars) in
     let npatt= deanonymize rids patt in
       List.rev (fst !rids),npatt in
-  let term2 =
-    GLetIn(Loc.ghost,Anonymous,
-	   GCast(Loc.ghost,glob_of_pat npatt,
-		 CastConv app_ind),term1) in
+  let term2=GLetIn(Loc.ghost,Anonymous,glob_of_pat npatt,Some app_ind,term1) in
   let term3=List.fold_right let_in_one_alias aliases term2 in
   let term4=List.fold_right prod_one_id loc_ids term3 in
   let term5=List.fold_right prod_one_hyp params term4 in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 8aab3b742..7dc869131 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -42,7 +42,7 @@ let compose_glob_context =
     match bt with
       | Lambda n -> mkGLambda(n,t,acc)
       | Prod n -> mkGProd(n,t,acc)
-      | LetIn n -> mkGLetIn(n,t,acc)
+      | LetIn n -> mkGLetIn(n,t,None,acc)
   in
   List.fold_right compose_binder
 
@@ -489,7 +489,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		    | u::l -> 
 			match t with 
 			  | GLambda(loc,na,_,nat,b) -> 
-			      GLetIn(Loc.ghost,na,u,aux b l)
+			      GLetIn(Loc.ghost,na,u,None,aux b l)
 			  | _ -> 
 			      GApp(Loc.ghost,t,l)
 		in
@@ -535,7 +535,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		      args_res.result
 		}
 	    | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *)
-       	    | GLetIn(_,n,t,b) ->
+	    | GLetIn(_,n,v,t,b) ->
 		(* if we have [(let x := v in b) t1 ... tn] ,
 		   we discard our work and compute the list of constructor for
 		   [let x = v in (b t1 ... tn)] up to alpha conversion
@@ -559,7 +559,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		  env
 		  funnames
 		  avoid
-		  (mkGLetIn(new_n,t,mkGApp(new_b,args)))
+		  (mkGLetIn(new_n,v,t,mkGApp(new_b,args)))
 	    | GCases _  | GIf _ | GLetTuple _ ->
 		(* we have [(match e1, ...., en with ..... end) t1 tn]
 		   we first compute the result from the case and
@@ -603,12 +603,13 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	let new_env = raw_push_named (n,None,t) env in
 	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_prod n) t_res b_res
-    | GLetIn(_,n,v,b) ->
+    | GLetIn(loc,n,v,typ,b) ->
 	(* we first compute the list of constructor
 	   corresponding to the body of the function,
 	   then the one corresponding to the value [t]
 	   and combine the two result
 	*)
+        let v = match typ with None -> v | Some t -> GCast (loc,v,CastConv t) in
 	let v_res = build_entry_lc env funnames avoid v in
 	let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
 	let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in
@@ -1118,8 +1119,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		(* We have renamed all the anonymous functions during alpha_renaming phase *)
 
 	end
-    | GLetIn(_,n,t,b) ->
+    | GLetIn(loc,n,v,t,b) ->
 	begin
+          let t = match t with None -> v | Some t -> GCast (loc,v,CastConv t) in
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let evd = (Evd.from_env env) in
 	  let t',ctx = Pretyping.understand env evd t in
@@ -1135,7 +1137,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  match n with
 	    | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args  ->
 		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
-	    | _ -> GLetIn(Loc.ghost,n,t,new_b),
+	    | _ -> GLetIn(Loc.ghost,n,t,None,new_b), (* HOPING IT WOULD WORK *)
 		Id.Set.filter not_free_in_t id_to_exclude
 	end
     | GLetTuple(_,nal,(na,rto),t,b) ->
@@ -1193,9 +1195,13 @@ let rec compute_cst_params relnames params = function
       compute_cst_params_from_app [] (params,rtl)
   | GApp(_,f,args) ->
       List.fold_left (compute_cst_params relnames) params (f::args)
-  | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetIn(_,_,t,b) | GLetTuple(_,_,_,t,b) ->
+  | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetTuple(_,_,_,t,b) ->
       let t_params = compute_cst_params relnames params t in
       compute_cst_params relnames t_params b
+  | GLetIn(_,_,v,t,b) ->
+      let v_params = compute_cst_params relnames params v in
+      let t_params = Option.fold_left (compute_cst_params relnames) v_params t in
+      compute_cst_params relnames t_params b
   | GCases _ ->
       params  (* If there is still cases at this point they can only be
 		 discrimination ones *)
@@ -1206,12 +1212,12 @@ let rec compute_cst_params relnames params = function
 and compute_cst_params_from_app acc (params,rtl) =
   match params,rtl with
     | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
-    | ((Name id,_,is_defined) as param)::params',(GVar(_,id'))::rtl'
-	when Id.compare id id' == 0 && not is_defined ->
+    | ((Name id,_,None) as param)::params',(GVar(_,id'))::rtl'
+	when Id.compare id id' == 0 ->
 	compute_cst_params_from_app (param::acc) (params',rtl')
     | _  -> List.rev acc
 
-let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) list array) csts =
+let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_constr option) list array) csts =
   let rels_params =
     Array.mapi
       (fun i args ->
@@ -1226,11 +1232,11 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool)
   let _ =
     try
       List.iteri
-	(fun i ((n,nt,is_defined) as param) ->
+	(fun i ((n,nt,typ) as param) ->
 	   if Array.for_all
 	     (fun l ->
-		let (n',nt',is_defined') = List.nth l i in
-		Name.equal n n' && glob_constr_eq nt nt' && (is_defined : bool) == is_defined')
+		let (n',nt',typ') = List.nth l i in
+		Name.equal n n' && glob_constr_eq nt nt' && Option.equal glob_constr_eq typ typ')
 	     rels_params
 	   then
 	     l := param::!l
@@ -1245,15 +1251,15 @@ let rec rebuild_return_type rt =
   match rt with
     | Constrexpr.CProdN(loc,n,t') ->
 	Constrexpr.CProdN(loc,n,rebuild_return_type t')
-    | Constrexpr.CLetIn(loc,na,t,t') ->
-	Constrexpr.CLetIn(loc,na,t,rebuild_return_type t')
+    | Constrexpr.CLetIn(loc,na,v,t,t') ->
+	Constrexpr.CLetIn(loc,na,v,t,rebuild_return_type t')
     | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Anonymous],
 				       Constrexpr.Default Decl_kinds.Explicit,rt],
 			    Constrexpr.CSort(Loc.ghost,GType []))
 
 
 let do_build_inductive
-      evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * bool) list list)
+      evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
       returned_types
       (rtl:glob_constr list) =
   let _time1 = System.get_time () in
@@ -1294,16 +1300,17 @@ let do_build_inductive
   let resa = Array.map (build_entry_lc env  funnames_as_set []) rta in
   let env_with_graphs =
     let rel_arity i funargs =  (* Rebuilding arities (with parameters) *)
-      let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list  =
+      let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list  =
 	funargs
       in
       List.fold_right
-	(fun (n,t,is_defined) acc ->
-	   if is_defined
-	   then
+	(fun (n,t,typ) acc ->
+          match typ with
+          | Some typ ->
 	     Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+                              Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
 			      acc)
-	   else
+	  | None ->
 	     Constrexpr.CProdN
 	       (Loc.ghost,
 		[[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
@@ -1361,16 +1368,17 @@ let do_build_inductive
     rel_constructors
   in
   let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
-    let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list  =
+    let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list  =
       (snd (List.chop nrel_params funargs))
     in
     List.fold_right
-      (fun (n,t,is_defined) acc ->
-	 if is_defined
-	 then
+      (fun (n,t,typ) acc ->
+         match typ with
+         | Some typ ->
 	   Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+                              Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
 			    acc)
-	 else
+	 | None ->
 	   Constrexpr.CProdN
 	   (Loc.ghost,
 	   [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
@@ -1397,12 +1405,13 @@ let do_build_inductive
   in
   let rel_params =
     List.map
-      (fun (n,t,is_defined) ->
-	 if is_defined
-	 then
-	   Constrexpr.LocalRawDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t)
-	 else
-	 Constrexpr.LocalRawAssum
+      (fun (n,t,typ) ->
+         match typ with
+         | Some typ ->
+	   Constrexpr.CLocalDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t,
+                                  Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ))
+	 | None ->
+	 Constrexpr.CLocalAssum
 	   ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
       )
       rels_params
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index 5bb1376e2..0cab5a6d3 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -12,7 +12,7 @@ val build_inductive :
  *)
   Evd.evar_map ->
   Term.pconstant list -> 
-  (Name.t*Glob_term.glob_constr*bool) list list -> (* The list of function args *)
+  (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list list -> (* The list of function args *)
   Constrexpr.constr_expr list -> (* The list of function returned type *)
   Glob_term.glob_constr list -> (* the list of body *)
   unit
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 4e561fc7e..99f50437b 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -15,7 +15,7 @@ let mkGVar id = GVar(Loc.ghost,id)
 let mkGApp(rt,rtl) = GApp(Loc.ghost,rt,rtl)
 let mkGLambda(n,t,b) = GLambda(Loc.ghost,n,Explicit,t,b)
 let mkGProd(n,t,b) = GProd(Loc.ghost,n,Explicit,t,b)
-let mkGLetIn(n,t,b) = GLetIn(Loc.ghost,n,t,b)
+let mkGLetIn(n,b,t,c) = GLetIn(Loc.ghost,n,b,t,c)
 let mkGCases(rto,l,brl) = GCases(Loc.ghost,Term.RegularStyle,rto,l,brl)
 let mkGSort s = GSort(Loc.ghost,s)
 let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None)
@@ -37,8 +37,8 @@ let glob_decompose_prod_or_letin =
   let rec glob_decompose_prod args = function
   | GProd(_,n,k,t,b) ->
       glob_decompose_prod ((n,None,Some t)::args) b
-  | GLetIn(_,n,t,b) ->
-      glob_decompose_prod ((n,Some t,None)::args) b
+  | GLetIn(_,n,b,t,c) ->
+      glob_decompose_prod ((n,Some b,t)::args) c
   | rt -> args,rt
   in
   glob_decompose_prod []
@@ -51,7 +51,7 @@ let glob_compose_prod_or_letin =
       fun concl decl ->
 	match decl with
 	  | (n,None,Some t) -> mkGProd(n,t,concl)
-	  | (n,Some bdy,None) -> mkGLetIn(n,bdy,concl)
+	  | (n,Some bdy,t) -> mkGLetIn(n,bdy,t,concl)
 	  | _ -> assert false)
 
 let glob_decompose_prod_n n =
@@ -73,8 +73,8 @@ let glob_decompose_prod_or_letin_n n =
       match c with
 	| GProd(_,n,_,t,b) ->
 	    glob_decompose_prod (i-1) ((n,None,Some t)::args) b
-	| GLetIn(_,n,t,b) ->
-	    glob_decompose_prod (i-1) ((n,Some t,None)::args) b
+	| GLetIn(_,n,b,t,c) ->
+	    glob_decompose_prod (i-1) ((n,Some b,t)::args) c
 	| rt -> args,rt
   in
   glob_decompose_prod n []
@@ -150,10 +150,11 @@ let change_vars =
 		  change_vars mapping t,
 		  change_vars (remove_name_from_mapping mapping name) b
 		 )
-      | GLetIn(loc,name,def,b) ->
+      | GLetIn(loc,name,def,typ,b) ->
 	  GLetIn(loc,
 		 name,
 		 change_vars mapping def,
+		 Option.map (change_vars mapping) typ,
 		 change_vars (remove_name_from_mapping mapping name) b
 		)
       | GLetTuple(loc,nal,(na,rto),b,e) ->
@@ -272,10 +273,11 @@ let rec alpha_rt excluded rt =
 	let new_t = alpha_rt excluded t in
 	let new_b = alpha_rt excluded b in
 	GProd(loc,Anonymous,k,new_t,new_b)
-    | GLetIn(loc,Anonymous,t,b) ->
-	let new_t = alpha_rt excluded t in
+    | GLetIn(loc,Anonymous,b,t,c) ->
 	let new_b = alpha_rt excluded b in
-	GLetIn(loc,Anonymous,new_t,new_b)
+	let new_t = Option.map (alpha_rt excluded) t in
+	let new_c = alpha_rt excluded c in
+	GLetIn(loc,Anonymous,new_b,new_t,new_c)
     | GLambda(loc,Name id,k,t,b) ->
 	let new_id = Namegen.next_ident_away id excluded in
 	let t,b =
@@ -302,19 +304,17 @@ let rec alpha_rt excluded rt =
 	let new_t = alpha_rt new_excluded t in
 	let new_b = alpha_rt new_excluded b in
 	GProd(loc,Name new_id,k,new_t,new_b)
-    | GLetIn(loc,Name id,t,b) ->
+    | GLetIn(loc,Name id,b,t,c) ->
 	let new_id = Namegen.next_ident_away id excluded in
-	let t,b =
-	  if Id.equal new_id id
-	  then t,b
-	  else
-	    let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in
-	    (t,replace b)
+	let c =
+	  if Id.equal new_id id then c
+	  else change_vars (Id.Map.add id new_id Id.Map.empty) c
 	in
 	let new_excluded = new_id::excluded in
-	let new_t = alpha_rt new_excluded t in
 	let new_b = alpha_rt new_excluded b in
-	GLetIn(loc,Name new_id,new_t,new_b)
+	let new_t = Option.map (alpha_rt new_excluded) t in
+	let new_c = alpha_rt new_excluded c in
+	GLetIn(loc,Name new_id,new_b,new_t,new_c)
 
 
     | GLetTuple(loc,nal,(na,rto),t,b) ->
@@ -388,13 +388,20 @@ let is_free_in id =
     | GEvar _ -> false
     | GPatVar _ -> false
     | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl)
-    | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) | GLetIn(_,n,t,b) ->
+    | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) ->
 	let check_in_b =
 	  match n with
 	    | Name id' -> not (Id.equal id' id)
 	    | _ -> true
 	in
 	is_free_in t || (check_in_b && is_free_in b)
+    | GLetIn(_,n,b,t,c) ->
+	let check_in_c =
+	  match n with
+	    | Name id' -> not (Id.equal id' id)
+	    | _ -> true
+	in
+	is_free_in b || Option.cata is_free_in true t || (check_in_c && is_free_in c)
     | GCases(_,_,_,el,brl) ->
 	(List.exists (fun (e,_) -> is_free_in e) el) ||
 	  List.exists is_free_in_br brl
@@ -473,11 +480,12 @@ let replace_var_by_term x_id term =
 		  replace_var_by_pattern t,
 		  replace_var_by_pattern b
 		 )
-      | GLetIn(_,Name id,_,_) when Id.compare id x_id == 0 -> rt
-      | GLetIn(loc,name,def,b) ->
+      | GLetIn(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt
+      | GLetIn(loc,name,def,typ,b) ->
 	  GLetIn(loc,
 		 name,
 		 replace_var_by_pattern def,
+		 Option.map (replace_var_by_pattern) typ,
 		 replace_var_by_pattern b
 		)
       | GLetTuple(_,nal,_,_,_)
@@ -589,7 +597,7 @@ let ids_of_glob_constr c =
           ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc
       | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
       | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
-      | GLetIn (loc,na,b,c) -> idof na :: ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc
+      | GLetIn (loc,na,b,t,c) -> idof na :: ids_of_glob_constr [] b @ Option.cata (ids_of_glob_constr []) [] t @ ids_of_glob_constr [] c @ acc
       | GCast (loc,c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc
       | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc
       | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc
@@ -633,9 +641,9 @@ let zeta_normalize =
 		zeta_normalize_term t,
 		zeta_normalize_term b
 		 )
-      | GLetIn(_,Name id,def,b) ->
+      | GLetIn(_,Name id,def,typ,b) ->
 	  zeta_normalize_term (replace_var_by_term id def b)
-      | GLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b
+      | GLetIn(loc,Anonymous,def,typ,b) -> zeta_normalize_term b
       | GLetTuple(loc,nal,(na,rto),def,b) ->
 	  GLetTuple(loc,
 		    nal,
@@ -690,7 +698,7 @@ let expand_as =
       | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args)
       | GLambda(loc,na,k,t,b) -> GLambda(loc,na,k,expand_as map t, expand_as map b)
       | GProd(loc,na,k,t,b) -> GProd(loc,na,k,expand_as map t, expand_as map b)
-      | GLetIn(loc,na,v,b) -> GLetIn(loc,na, expand_as map v,expand_as map b)
+      | GLetIn(loc,na,v,typ,b) -> GLetIn(loc,na, expand_as map v,Option.map (expand_as map) typ,expand_as map b)
       | GLetTuple(loc,nal,(na,po),v,b) ->
 	  GLetTuple(loc,nal,(na,Option.map (expand_as map) po),
 		    expand_as map v, expand_as map b)
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 179e8fe8d..84359a36b 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -19,7 +19,7 @@ val mkGVar : Id.t -> glob_constr
 val mkGApp  : glob_constr*(glob_constr list) -> glob_constr
 val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr
 val mkGProd : Name.t * glob_constr * glob_constr -> glob_constr
-val mkGLetIn : Name.t * glob_constr * glob_constr -> glob_constr
+val mkGLetIn : Name.t * glob_constr * glob_constr option * glob_constr -> glob_constr
 val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr
 val mkGSort : glob_sort -> glob_constr
 val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2852152e1..ebeddf5f6 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -134,11 +134,11 @@ let functional_induction with_clean c princl pat =
 
 let rec abstract_glob_constr c = function
   | [] -> c
-  | Constrexpr.LocalRawDef (x,b)::bl -> Constrexpr_ops.mkLetInC(x,b,abstract_glob_constr c bl)
-  | Constrexpr.LocalRawAssum (idl,k,t)::bl ->
+  | Constrexpr.CLocalDef (x,b,t)::bl -> Constrexpr_ops.mkLetInC(x,b,t,abstract_glob_constr c bl)
+  | Constrexpr.CLocalAssum (idl,k,t)::bl ->
       List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl
         (abstract_glob_constr c bl)
-  | Constrexpr.LocalPattern _::bl -> assert false
+  | Constrexpr.CLocalPattern _::bl -> assert false
 
 let interp_casted_constr_with_implicits env sigma impls c  =
   Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
@@ -197,8 +197,10 @@ let is_rec names =
     | GRec _ -> error "GRec not handled"
     | GIf(_,b,_,lhs,rhs) ->
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
-    | GLetIn(_,na,t,b) | GLambda(_,na,_,t,b) | GProd(_,na,_,t,b)  ->
+    | GProd(_,na,_,t,b) | GLambda(_,na,_,t,b) ->
 	lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b
+    | GLetIn(_,na,b,t,c) ->
+	lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c
     | GLetTuple(_,nal,_,t,b) -> lookup names t ||
 	lookup
 	  (List.fold_left
@@ -220,9 +222,9 @@ let is_rec names =
 let rec local_binders_length = function
   (* Assume that no `{ ... } contexts occur *)
   | [] -> 0
-  | Constrexpr.LocalRawDef _::bl -> 1 + local_binders_length bl
-  | Constrexpr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
-  | Constrexpr.LocalPattern _::bl -> assert false
+  | Constrexpr.CLocalDef _::bl -> 1 + local_binders_length bl
+  | Constrexpr.CLocalAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
+  | Constrexpr.CLocalPattern _::bl -> assert false
 
 let prepare_body ((name,_,args,types,_),_) rt =
   let n = local_binders_length args in
@@ -511,7 +513,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
       | None ->
 	  begin
 	    match args with
-	      | [Constrexpr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x
+	      | [Constrexpr.CLocalAssum ([(_,Name x)],k,t)] -> t,x
 	      | _ -> error "Recursive argument must be specified"
 	  end
       | Some wf_args ->
@@ -519,7 +521,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 	    match
 	      List.find
 		(function
-		   | Constrexpr.LocalRawAssum(l,k,t) ->
+		   | Constrexpr.CLocalAssum(l,k,t) ->
 		       List.exists
 			 (function (_,Name id) -> Id.equal id wf_args | _ -> false)
 			 l
@@ -527,7 +529,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 		)
 		args
 	    with
-	      | Constrexpr.LocalRawAssum(_,k,t)  ->	    t,wf_args
+	      | Constrexpr.CLocalAssum(_,k,t)  ->	    t,wf_args
 	      | _ -> assert false
 	  with Not_found -> assert false
   in
@@ -585,10 +587,10 @@ let make_assoc assoc l1 l2 =
 let rec rebuild_bl (aux,assoc) bl typ = 
 	match bl,typ with 
 	  | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc)
-	  | (Constrexpr.LocalRawAssum(nal,bk,_))::bl',typ ->
+	  | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ ->
 	     rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ
-	  | (Constrexpr.LocalRawDef(na,_))::bl',Constrexpr.CLetIn(_,_,nat,typ') ->
-	    rebuild_bl ((Constrexpr.LocalRawDef(na,replace_vars_constr_expr assoc nat)::aux),assoc)
+	  | (Constrexpr.CLocalDef(na,_,_))::bl',Constrexpr.CLetIn(_,_,nat,ty,typ') ->
+	    rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc)
 	      bl' typ'
 	  | _ -> assert false
       and rebuild_nal (aux,assoc) bk bl' nal lnal typ = 
@@ -601,7 +603,7 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	    then 
 	      let old_nal',new_nal' = List.chop lnal nal' in
 	      let nassoc = make_assoc assoc old_nal' nal in
-	      let assum = LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't) in
+	      let assum = CLocalAssum(nal,bk,replace_vars_constr_expr assoc nal't) in
 	      rebuild_bl ((assum :: aux), nassoc) bl' 
 		(if List.is_empty new_nal' && List.is_empty rest
 		 then typ'
@@ -611,7 +613,7 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	    else 
 	      let captured_nal,non_captured_nal = List.chop lnal' nal in
 	      let nassoc = make_assoc assoc nal' captured_nal in
-	      let assum = LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in
+	      let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in
 	      rebuild_nal ((assum :: aux), nassoc)
 		bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ'))
 	  | _ -> assert false
@@ -741,8 +743,8 @@ let rec add_args id new_args b =
       CLambdaN(loc,
 	       List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args  b2)) nal,
 	       add_args id new_args  b1)
-  | CLetIn(loc,na,b1,b2) ->
-      CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
+  | CLetIn(loc,na,b1,t,b2) ->
+      CLetIn(loc,na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2)
   | CAppExpl(loc,(pf,r,us),exprl) ->
       begin
 	match r with
@@ -828,7 +830,7 @@ let rec chop_n_arrow n t =
       | _ -> anomaly (Pp.str "Not enough products")
 
 
-let rec get_args b t : Constrexpr.local_binder list *
+let rec get_args b t : Constrexpr.local_binder_expr list *
     Constrexpr.constr_expr * Constrexpr.constr_expr =
   match b with
     | Constrexpr.CLambdaN (loc, (nal_ta), b') ->
@@ -839,7 +841,7 @@ let rec get_args b t : Constrexpr.local_binder list *
 	  in
 	  let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in
 	  (List.map (fun (nal,k,ta) ->
-		       (Constrexpr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t''
+		       (Constrexpr.CLocalAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t''
 	end
     | _ -> [],b,t
 
@@ -880,13 +882,13 @@ let make_graph (f_ref:global_reference) =
 			  List.flatten
 			    (List.map
 			       (function
-				  | Constrexpr.LocalRawDef (na,_)-> []
-				  | Constrexpr.LocalRawAssum (nal,_,_) ->
+				  | Constrexpr.CLocalDef (na,_,_)-> []
+				  | Constrexpr.CLocalAssum (nal,_,_) ->
 				      List.map
 					(fun (loc,n) ->
 					   CRef(Libnames.Ident(loc, Nameops.out_name n),None))
 					nal
-                                  | Constrexpr.LocalPattern _ -> assert false
+                                  | Constrexpr.CLocalPattern _ -> assert false
 			       )
 			       nal_tas
 			    )
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 2889d8d03..20da12f39 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -70,8 +70,8 @@ let chop_rlambda_n  =
       then List.rev acc,rt
       else
 	match rt with
-	  | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
-	  | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
+	  | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b
+	  | Glob_term.GLetIn(_,name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b
 	  | _ ->
 	      raise (CErrors.UserError(Some "chop_rlambda_n",
 				    str "chop_rlambda_n: Not enough Lambdas"))
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 5836d6519..5c3e73e9d 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -34,7 +34,7 @@ val list_add_set_eq :
   ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
 
 val chop_rlambda_n : int -> Glob_term.glob_constr ->
-  (Name.t*Glob_term.glob_constr*bool) list * Glob_term.glob_constr
+  (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list * Glob_term.glob_constr
 
 val chop_rprod_n : int -> Glob_term.glob_constr ->
   (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index c0298d06c..f1ca57585 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -512,14 +512,14 @@ let rec merge_app c1 c2 id1 id2 shift filter_shift_stable =
         let args = filter_shift_stable lnk (arr1 @ arr2) in
         GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args)
     | GApp(_,f1, arr1), GApp(_,f2,arr2)  -> raise NoMerge
-    | GLetIn(_,nme,bdy,trm) , _ ->
+    | GLetIn(_,nme,bdy,typ,trm) , _ ->
         let _ = prstr "\nICI2!\n" in
         let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
-        GLetIn(Loc.ghost,nme,bdy,newtrm)
-    | _, GLetIn(_,nme,bdy,trm) ->
+        GLetIn(Loc.ghost,nme,bdy,typ,newtrm)
+    | _, GLetIn(_,nme,bdy,typ,trm) ->
         let _ = prstr "\nICI3!\n" in
         let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
-        GLetIn(Loc.ghost,nme,bdy,newtrm)
+        GLetIn(Loc.ghost,nme,bdy,typ,newtrm)
     | _ -> let _ = prstr "\nICI4!\n" in
            raise NoMerge
 
@@ -530,14 +530,14 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
         let args = filter_shift_stable lnk (arr1 @ arr2) in
         GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args)
           (* FIXME: what if the function appears in the body of the let? *)
-    | GLetIn(_,nme,bdy,trm) , _ ->
+    | GLetIn(_,nme,bdy,typ,trm) , _ ->
       let _ = prstr "\nICI2 '!\n" in
         let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
-        GLetIn(Loc.ghost,nme,bdy,newtrm)
-    | _, GLetIn(_,nme,bdy,trm) ->
+        GLetIn(Loc.ghost,nme,bdy,typ,newtrm)
+    | _, GLetIn(_,nme,bdy,typ,trm) ->
         let _ = prstr "\nICI3 '!\n" in
         let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
-        GLetIn(Loc.ghost,nme,bdy,newtrm)
+        GLetIn(Loc.ghost,nme,bdy,typ,newtrm)
     | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge
 
 
@@ -825,7 +825,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
         let _ = prNamedRConstr (string_of_name nme) tp in
         let _ = prstr "  ;  " in
         let typ = glob_constr_to_constr_expr tp in
-        LocalRawAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
+        CLocalAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
       [] params in
   let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in
   let arity,_ =
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index aab568746..fd33a779d 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+DECLARE PLUGIN "ltac_plugin"
+
 open Util
 open Pp
 open Compat
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index d286a5870..3e6e2db60 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -70,7 +70,7 @@ GEXTEND Gram
   Constr.closed_binder:
     [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
 	  let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
-          [LocalRawAssum ([id], default_binder_kind, typ)]
+          [CLocalAssum ([id], default_binder_kind, typ)]
     ] ];
 
   END
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index b1c4f58eb..c50100bf5 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -183,7 +183,7 @@ VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF
       [ declare_relation a aeq n None None (Some lemma3) ]
 END
 
-type binders_argtype = local_binder list
+type binders_argtype = local_binder_expr list
 
 let wit_binders =
  (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type)
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 10fec2032..7a20838a2 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -78,17 +78,17 @@ val is_applied_rewrite_relation :
   env -> evar_map -> rel_context -> constr -> types option
 
 val declare_relation :
-  ?binders:local_binder list -> constr_expr -> constr_expr -> Id.t ->
+  ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t ->
   constr_expr option -> constr_expr option -> constr_expr option -> unit
 
 val add_setoid :
-  bool -> local_binder list -> constr_expr -> constr_expr -> constr_expr ->
+  bool -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
   Id.t -> unit
 
 val add_morphism_infer : bool -> constr_expr -> Id.t -> unit
 
 val add_morphism :
-  bool -> local_binder list -> constr_expr -> constr_expr -> Id.t -> unit
+  bool -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit
 
 val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
 
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 01e20d0f1..3150d6a1b 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -156,7 +156,7 @@ let mkCHole loc = CHole (loc, None, IntroAnonymous, None)
 let mkCLambda loc name ty t = 
    CLambdaN (loc, [[loc, name], Default Explicit, ty], t)
 let mkCLetIn loc name bo t = 
-   CLetIn (loc, (loc, name), bo, t)
+   CLetIn (loc, (loc, name), bo, None, t)
 let mkCCast loc t ty = CCast (loc,t, dC ty)
 (** Constructors for rawconstr *)
 let mkRHole = GHole (dummy_loc, InternalHole, IntroAnonymous, None)
@@ -1204,7 +1204,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
   pp(lazy(str"typed as: " ++ pr_pattern_w_ids red));
   let mkXLetIn loc x (a,(g,c)) = match c with
   | Some b -> a,(g,Some (mkCLetIn loc x (mkCHole loc) b))
-  | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), g), None) in
+  | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), None, g), None) in
   match red with
   | T t -> let sigma, t = interp_term ist gl t in sigma, T t
   | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t