merging conflicts with the original "trunk__CLEANUP__Context__2" branch

4 files changed, 20 insertions, 16 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 9cdcb9e38..367544135 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -29,6 +29,8 @@ open Notation
 open Detyping
 open Misctypes
 open Decl_kinds
+
+module NamedDecl = Context.Named.Declaration
 (*i*)
 
 (* Translation from glob_constr to front constr *)
@@ -980,7 +982,7 @@ let rec glob_of_pat env sigma = function
   | PRef ref -> GRef (loc,ref,None)
   | PVar id -> GVar (loc,id)
   | PEvar (evk,l) ->
-      let test (id,_,_) = function PVar id' -> Id.equal id id' | _ -> false in
+      let test decl = function PVar id' -> Id.equal (NamedDecl.get_id decl) id' | _ -> false in
       let l = Evd.evar_instance_array test (Evd.find sigma evk) l in
       let id = match Evd.evar_ident evk sigma with
       | None -> Id.of_string "__"
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 964ed0514..70802d5cb 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -29,6 +29,7 @@ open Nametab
 open Notation
 open Inductiveops
 open Decl_kinds
+open Context.Rel.Declaration
 
 (** constr_expr -> glob_constr translation:
     - it adds holes for implicit arguments
@@ -1645,14 +1646,14 @@ let internalize globalenv env allow_patvar lvar c =
 	      |loc,(Name y as x) -> (y,PatVar(loc,x)) :: l in
 	    match case_rel_ctxt,arg_pats with
 	      (* LetIn in the rel_context *)
-	      |(_,Some _,_)::t, l when not with_letin ->
+	      | LocalDef _ :: t, l when not with_letin ->
 		canonize_args t l forbidden_names match_acc ((Loc.ghost,Anonymous)::var_acc)
 	      |[],[] ->
 		(add_name match_acc na, var_acc)
 	      |_::t,PatVar (loc,x)::tt ->
 		canonize_args t tt forbidden_names
 		  (add_name match_acc (loc,x)) ((loc,x)::var_acc)
-	      |(cano_name,_,ty)::t,c::tt ->
+	      | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt ->
 		let fresh =
 		  Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names ty in
 		canonize_args t tt (fresh::forbidden_names)
@@ -1894,7 +1895,7 @@ let interp_rawcontext_evars env evdref k bl =
 	      let t' = locate_if_hole (loc_of_glob_constr t) na t in
 	      let t =
                 understand_tcc_evars env evdref ~expected_type:IsType t' in
-	      let d = (na,None,t) in
+	      let d = LocalAssum (na,t) in
 	      let impls =
 		if k == Implicit then
 		  let na = match na with Name n -> Some n | Anonymous -> None in
@@ -1904,7 +1905,7 @@ let interp_rawcontext_evars env evdref k bl =
 		(push_rel d env, d::params, succ n, impls)
 	  | Some b ->
 	      let c = understand_judgment_tcc env evdref b in
-	      let d = (na, Some c.uj_val, c.uj_type) in
+	      let d = LocalDef (na, c.uj_val, c.uj_type) in
 		(push_rel d env, d::params, n, impls))
       (env,[],k+1,[]) (List.rev bl)
   in (env, par), impls
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 391c600ed..751b03a4a 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -20,6 +20,7 @@ open Pp
 open Libobject
 open Nameops
 open Misctypes
+open Context.Rel.Declaration
 (*i*)
 
 let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident"
@@ -196,7 +197,7 @@ let combine_params avoid fn applied needed =
     List.partition
       (function
 	  (t, Some (loc, ExplByName id)) ->
-            let is_id (_, (na, _, _)) = match na with
+            let is_id (_, decl) = match get_name decl with
             | Name id' -> Id.equal id id'
             | Anonymous -> false
             in
@@ -209,22 +210,22 @@ let combine_params avoid fn applied needed =
     (fun x -> match x with (t, Some (loc, ExplByName id)) -> id, t | _ -> assert false)
     named
   in
-  let is_unset (_, (_, b, _)) = match b with
-  | None -> true
-  | Some _ -> false
+  let is_unset (_, decl) = match decl with
+  | LocalAssum _ -> true
+  | LocalDef _ -> false
   in
   let needed = List.filter is_unset needed in
   let rec aux ids avoid app need =
     match app, need with
 	[], [] -> List.rev ids, avoid
 
-      | app, (_, (Name id, _, _)) :: need when Id.List.mem_assoc id named ->
+      | app, (_, (LocalAssum (Name id, _) | LocalDef (Name id, _, _))) :: need when Id.List.mem_assoc id named ->
 	  aux (Id.List.assoc id named :: ids) avoid app need
 
-      | (x, None) :: app, (None, (Name id, _, _)) :: need ->
+      | (x, None) :: app, (None, (LocalAssum (Name id, _) | LocalDef (Name id, _, _))) :: need ->
 	  aux (x :: ids) avoid app need
 
-      | _, (Some cl, (_, _, _) as d) :: need ->
+      | _, (Some cl, _ as d) :: need ->
 	  let t', avoid' = fn avoid d in
 	    aux (t' :: ids) avoid' app need
 
@@ -239,8 +240,8 @@ let combine_params avoid fn applied needed =
   in aux [] avoid applied needed
 
 let combine_params_freevar =
-  fun avoid (_, (na, _, _)) ->
-    let id' = next_name_away_from na avoid in
+  fun avoid (_, decl) ->
+    let id' = next_name_away_from (get_name decl) avoid in
       (CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid)
 
 let destClassApp cl =
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index b226bfa0a..d0327e506 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -38,10 +38,10 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
 val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
 
 val combine_params_freevar :
-  Id.Set.t -> (global_reference * bool) option * (Name.t * Term.constr option * Term.types) ->
+  Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t ->
   Constrexpr.constr_expr * Id.Set.t
 
 val implicit_application : Id.Set.t -> ?allow_partial:bool ->
-  (Id.Set.t -> (global_reference * bool) option * (Name.t * Term.constr option * Term.types) ->
+  (Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t ->
     Constrexpr.constr_expr * Id.Set.t) ->
   constr_expr -> constr_expr * Id.Set.t