Merge PR#379: Introducing evar-insensitive constrs

7 files changed, 28 insertions, 19 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 925e9517c7..f272d219aa 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -961,6 +961,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t =
   (* Not "goal_concl_style" means do alpha-conversion avoiding only *)
   (* those goal/section/rel variables that occurs in the subterm under *)
   (* consideration; see namegen.ml for further details *)
+  let t = EConstr.of_constr t in
   let avoid = if goal_concl_style then ids_of_context env else [] in
   let r = Detyping.detype ~lax:lax goal_concl_style avoid env sigma t in
   let vars = vars_of_env env in
@@ -973,6 +974,7 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t =
   extern_constr_gen lax goal_concl_style None env sigma t
 
 let extern_type goal_concl_style env sigma t =
+  let t = EConstr.of_constr t in
   let avoid = if goal_concl_style then ids_of_context env else [] in
   let r = Detyping.detype goal_concl_style avoid env sigma t in
   extern_glob_type (vars_of_env env) r
@@ -1051,14 +1053,16 @@ let rec glob_of_pat env sigma = function
 	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive")
       in
       GCases (loc,RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
-  | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (mkFix f) (** FIXME bad env *)
-  | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (mkCoFix c)
+  | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f)) (** FIXME bad env *)
+  | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))
   | PSort s -> GSort (loc,s)
 
 let extern_constr_pattern env sigma pat =
   extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat)
 
 let extern_rel_context where env sigma sign =
+  let sign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) sign in
+  let where = Option.map EConstr.of_constr where in
   let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in
   let vars = vars_of_env env in
   let a = List.map (extended_glob_local_binder_of_decl Loc.ghost) a in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8fe6ce85e8..d75487ecf3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1831,7 +1831,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 		  (add_name match_acc (loc,x)) ((loc,x)::var_acc)
 	      | (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
+		  Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in
 		canonize_args t tt (fresh::forbidden_names)
 		  ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc)
 	      | _ -> assert false in
@@ -1925,7 +1925,7 @@ let extract_ids env =
 
 let scope_of_type_kind = function
   | IsType -> Notation.current_type_scope_name ()
-  | OfType typ -> compute_type_scope typ
+  | OfType typ -> compute_type_scope (EConstr.Unsafe.to_constr typ)
   | WithoutTypeConstraint -> None
 
 let empty_ltac_sign = {
@@ -2004,7 +2004,7 @@ let interp_constr_evars env evdref ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c
 
 let interp_casted_constr_evars env evdref ?(impls=empty_internalization_env) c typ =
-  interp_constr_evars_gen env evdref ~impls (OfType typ) c
+  interp_constr_evars_gen env evdref ~impls (OfType (EConstr.of_constr typ)) c
 
 let interp_type_evars env evdref ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen env evdref IsType ~impls c
@@ -2064,6 +2064,7 @@ let intern_context global_level env impl_env binders =
     user_err ~loc ~hdr:"internalize" (explain_internalization_error e)
 
 let interp_rawcontext_evars env evdref k bl =
+  let open EConstr in
   let (env, par, _, impls) =
     List.fold_left
       (fun (env,params,n,impls) (na, k, b, t) ->
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index e45de25887..758d4e650b 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -99,7 +99,7 @@ val interp_constr : env -> evar_map -> ?impls:internalization_env ->
   constr_expr -> constr Evd.in_evar_universe_context
 
 val interp_casted_constr : env -> evar_map -> ?impls:internalization_env ->
-  constr_expr -> types -> constr Evd.in_evar_universe_context
+  constr_expr -> EConstr.types -> constr Evd.in_evar_universe_context
 
 val interp_type : env -> evar_map -> ?impls:internalization_env ->
   constr_expr -> types Evd.in_evar_universe_context
@@ -107,32 +107,32 @@ val interp_type : env -> evar_map -> ?impls:internalization_env ->
 (** Main interpretation function expecting all postponed problems to
     be resolved, but possibly leaving evars. *)
 
-val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr
+val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * EConstr.constr
 
 (** Accepting unresolved evars *)
 
 val interp_constr_evars : env -> evar_map ref ->
-  ?impls:internalization_env -> constr_expr -> constr
+  ?impls:internalization_env -> constr_expr -> EConstr.constr
 
 val interp_casted_constr_evars : env -> evar_map ref ->
-  ?impls:internalization_env -> constr_expr -> types -> constr
+  ?impls:internalization_env -> constr_expr -> types -> EConstr.constr
 
 val interp_type_evars : env -> evar_map ref ->
-  ?impls:internalization_env -> constr_expr -> types
+  ?impls:internalization_env -> constr_expr -> EConstr.types
 
 (** Accepting unresolved evars and giving back the manual implicit arguments *)
 
 val interp_constr_evars_impls : env -> evar_map ref ->
   ?impls:internalization_env -> constr_expr ->
-  constr * Impargs.manual_implicits
+  EConstr.constr * Impargs.manual_implicits
 
 val interp_casted_constr_evars_impls : env -> evar_map ref ->
-  ?impls:internalization_env -> constr_expr -> types ->
-  constr * Impargs.manual_implicits
+  ?impls:internalization_env -> constr_expr -> EConstr.types ->
+  EConstr.constr * Impargs.manual_implicits
 
 val interp_type_evars_impls : env -> evar_map ref ->
   ?impls:internalization_env -> constr_expr ->
-  types * Impargs.manual_implicits
+  EConstr.types * Impargs.manual_implicits
 
 (** Interprets constr patterns *)
 
@@ -151,14 +151,14 @@ val interp_reference : ltac_sign -> reference -> glob_constr
 val interp_binder  : env -> evar_map -> Name.t -> constr_expr -> 
   types Evd.in_evar_universe_context
 
-val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types
+val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConstr.types
 
 (** Interpret contexts: returns extended env and context *)
 
 val interp_context_evars :
   ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
   env -> evar_map ref -> local_binder_expr list ->
-  internalization_env * ((env * Context.Rel.t) * Impargs.manual_implicits)
+  internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits)
 
 (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
 (*   (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)
@@ -175,7 +175,7 @@ val interp_context_evars :
 
 val locate_reference :  Libnames.qualid -> Globnames.global_reference
 val is_global : Id.t -> bool
-val construct_reference : Context.Named.t -> Id.t -> constr
+val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> constr
 val global_reference : Id.t -> constr
 val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 66d3c91859..90ac7f7296 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -585,7 +585,7 @@ let scope_class_compare : scope_class -> scope_class -> int =
   cl_typ_ord
 
 let compute_scope_class t =
-  let (cl,_,_) = find_class_type Evd.empty t in
+  let (cl,_,_) = find_class_type Evd.empty (EConstr.of_constr t) in
   cl
 
 module ScopeClassOrd =
@@ -615,7 +615,7 @@ let find_scope_class_opt = function
 (* Special scopes associated to arguments of a global reference *)
 
 let rec compute_arguments_classes t =
-  match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty t) with
+  match kind_of_term (EConstr.Unsafe.to_constr (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t))) with
     | Prod (_,t,u) ->
 	let cl = try Some (compute_scope_class t) with Not_found -> None in
 	cl :: compute_arguments_classes u
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 59625426f0..8b4fadb5a0 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -442,6 +442,7 @@ let notation_constr_of_glob_constr nenv a =
 (* Substitution of kernel names, avoiding a list of bound identifiers *)
 
 let notation_constr_of_constr avoiding t =
+  let t = EConstr.of_constr t in
   let t = Detyping.detype false avoiding (Global.env()) Evd.empty t in
   let nenv = {
     ninterp_var_type = Id.Map.empty;
diff --git a/interp/reserve.ml b/interp/reserve.ml
index a4d4f40277..1565ba4a92 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -107,7 +107,9 @@ let constr_key c =
 
 let revert_reserved_type t =
   try
+    let t = EConstr.Unsafe.to_constr t in
     let reserved = KeyMap.find (constr_key t) !reserve_revtable in
+    let t = EConstr.of_constr t in
     let t = Detyping.detype false [] (Global.env()) Evd.empty t in
     (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
         then I've introduced a bug... *)
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index af3a734627..113fe40ba7 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -11,6 +11,7 @@
 open Loc
 open Names
 open Term
+open EConstr
 open Libnames
 open Globnames
 open Genredexpr