Detyping functions are now operating on EConstr.t.

This was already the case, but the API was not exposing this.

8 files changed, 35 insertions, 37 deletions

diff --git a/API/API.mli b/API/API.mli
index a0e77edd1..f3ed7a894 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4283,10 +4283,10 @@ module Constrextern :
 sig
   val extern_glob_constr : Names.Id.Set.t -> Glob_term.glob_constr -> Constrexpr.constr_expr
   val extern_glob_type : Names.Id.Set.t -> Glob_term.glob_constr -> Constrexpr.constr_expr
-  val extern_constr : ?lax:bool -> bool -> Environ.env -> Evd.evar_map -> Constr.t -> Constrexpr.constr_expr
+  val extern_constr : ?lax:bool -> bool -> Environ.env -> Evd.evar_map -> EConstr.t -> Constrexpr.constr_expr
   val without_symbols : ('a -> 'b) -> 'a -> 'b
   val print_universes : bool ref
-  val extern_type : bool -> Environ.env -> Evd.evar_map -> Term.types -> Constrexpr.constr_expr
+  val extern_type : bool -> Environ.env -> Evd.evar_map -> EConstr.t -> Constrexpr.constr_expr
   val with_universes : ('a -> 'b) -> 'a -> 'b
   val set_extern_reference :
     (?loc:Loc.t -> Names.Id.Set.t -> Globnames.global_reference -> Libnames.reference) -> unit
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fcaee5c93..54861ae4c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1098,7 +1098,6 @@ 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
@@ -1111,7 +1110,6 @@ 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
@@ -1198,8 +1196,6 @@ 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) a in
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index b5242b347..ffa891c50 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -9,6 +9,7 @@
 open Names
 open Term
 open Termops
+open EConstr
 open Environ
 open Libnames
 open Globnames
@@ -41,7 +42,7 @@ val extern_reference : ?loc:Loc.t -> Id.Set.t -> global_reference -> reference
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
 val extern_sort : Evd.evar_map -> sorts -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
-  Context.Rel.t -> local_binder_expr list
+  rel_context -> local_binder_expr list
 
 (** Printing options *)
 val print_implicits : bool ref
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 5ba98fb58..05194164b 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -233,7 +233,7 @@ let extend_with_auto_hints env sigma l seq =
 
 let print_cmap map=
   let print_entry c l s=
-    let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty c in
+    let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty (EConstr.of_constr c) in
       str "| " ++
       prlist Printer.pr_global l ++
       str " : " ++
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 89537ad3f..8769f5668 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -618,7 +618,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
   let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
   let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in
   let constr_expr_typel = 
-    with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx))) typel in
+    with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
   let fixpoint_exprl_with_new_bl = 
     List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> 
      
@@ -855,9 +855,9 @@ let make_graph (f_ref:global_reference) =
 	 let sigma = Evd.from_env env in
 	 let extern_body,extern_type =
 	   with_full_print (fun () ->
-		(Constrextern.extern_constr false env sigma body,
+		(Constrextern.extern_constr false env sigma (EConstr.of_constr body),
 		 Constrextern.extern_type false env sigma
-                   ((*FIXME*) c_body.const_type)
+                   (EConstr.of_constr (*FIXME*) c_body.const_type)
 		)
 	     )
 	     ()
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 52a82b0e5..3ae922190 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -812,13 +812,13 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
         let typ = glob_constr_to_constr_expr tp in
         CLocalAssum ([(Loc.tag nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
       [] params in
-  let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in
+  let concl = Constrextern.extern_constr false (Global.env()) Evd.empty (EConstr.of_constr concl) in
   let arity,_ =
     List.fold_left
       (fun (acc,env) decl ->
         let nm = Context.Rel.Declaration.get_name decl in
         let c = RelDecl.get_type decl in
-        let typ = Constrextern.extern_constr false env Evd.empty c in
+        let typ = Constrextern.extern_constr false env Evd.empty (EConstr.of_constr c) in
         let newenv = Environ.push_rel (LocalAssum (nm,c)) env in
         CAst.make @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
       (concl,Global.env())
diff --git a/printing/printer.ml b/printing/printer.ml
index c6cf2254f..0d8168be9 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -79,23 +79,23 @@ let _ =
    and only names of goal/section variables and rel names that do
    _not_ occur in the scope of the binder to be printed are avoided. *)
 
-let pr_constr_core goal_concl_style env sigma t =
+let pr_econstr_core goal_concl_style env sigma t =
   pr_constr_expr (extern_constr goal_concl_style env sigma t)
-let pr_lconstr_core goal_concl_style env sigma t =
+let pr_leconstr_core goal_concl_style env sigma t =
   pr_lconstr_expr (extern_constr goal_concl_style env sigma t)
 
-let pr_lconstr_env env = pr_lconstr_core false env
-let pr_constr_env env = pr_constr_core false env
+let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c)
+let pr_constr_env env sigma c = pr_econstr_core false env sigma (EConstr.of_constr c)
 let _ = Hook.set Refine.pr_constr pr_constr_env
 
-let pr_lconstr_goal_style_env env = pr_lconstr_core true env
-let pr_constr_goal_style_env env = pr_constr_core true env
+let pr_lconstr_goal_style_env env sigma c = pr_leconstr_core true env sigma (EConstr.of_constr c)
+let pr_constr_goal_style_env env sigma c = pr_econstr_core true env sigma (EConstr.of_constr c)
 
 let pr_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c
 let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c
 
-let pr_leconstr_env env sigma c = pr_lconstr_env env sigma (EConstr.to_constr sigma c)
-let pr_econstr_env env sigma c = pr_constr_env env sigma (EConstr.to_constr sigma c)
+let pr_leconstr_env env sigma c = pr_leconstr_core false env sigma c
+let pr_econstr_env env sigma c = pr_econstr_core false env sigma c
 
 (* NB do not remove the eta-redexes! Global.env() has side-effects... *)
 let pr_lconstr t =
@@ -128,13 +128,13 @@ let pr_lconstr_under_binders c =
   let (sigma, env) = get_current_context () in
   pr_lconstr_under_binders_env env sigma c
 
-let pr_type_core goal_concl_style env sigma t =
+let pr_etype_core goal_concl_style env sigma t =
   pr_constr_expr (extern_type goal_concl_style env sigma t)
-let pr_ltype_core goal_concl_style env sigma t =
+let pr_letype_core goal_concl_style env sigma t =
   pr_lconstr_expr (extern_type goal_concl_style env sigma t)
 
-let pr_ltype_env env = pr_ltype_core false env
-let pr_type_env env = pr_type_core false env
+let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr c)
+let pr_type_env env sigma c = pr_etype_core false env sigma (EConstr.of_constr c)
 
 let pr_ltype t =
     let (sigma, env) = get_current_context () in
@@ -143,10 +143,9 @@ let pr_type t =
     let (sigma, env) = get_current_context () in
     pr_type_env env sigma t
 
-let pr_etype_env env sigma c = pr_type_env env sigma (EConstr.to_constr sigma c)
-let pr_letype_env env sigma c = pr_ltype_env env sigma (EConstr.to_constr sigma c)
-let pr_goal_concl_style_env env sigma c =
-  pr_ltype_core true env sigma (EConstr.to_constr sigma c)
+let pr_etype_env env sigma c = pr_etype_core false env sigma c
+let pr_letype_env env sigma c = pr_letype_core false env sigma c
+let pr_goal_concl_style_env env sigma c = pr_letype_core true env sigma c
 
 let pr_ljudge_env env sigma j =
   (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type)
@@ -191,7 +190,7 @@ let pr_constr_pattern t =
 let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
 
 let _ = Termops.set_print_constr 
-  (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma (EConstr.Unsafe.to_constr t)))
+  (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t))
 
 let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
 
@@ -364,6 +363,7 @@ let pr_named_context env sigma ne_context =
           ne_context ~init:(mt ()))
 
 let pr_rel_context env sigma rel_context =
+  let rel_context = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) rel_context in
   pr_binders (extern_rel_context None env sigma rel_context)
 
 let pr_rel_context_of env sigma =
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 0e5184905..2be10a039 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -100,17 +100,18 @@ let pr_ljudge_env e s c = let v,t = pr_ljudge_env e s c in (quote v,quote t)
 
 (** A canonisation procedure for constr such that comparing there
     externalisation catches more equalities *)
-let canonize_constr c =
+let canonize_constr sigma c =
   (* replaces all the names in binders by [dn] ("default name"),
      ensures that [alpha]-equivalent terms will have the same
      externalisation. *)
+  let open EConstr in
   let dn = Name.Anonymous in
   let rec canonize_binders c =
-    match Term.kind_of_term c with
+    match EConstr.kind sigma c with
     | Prod (_,t,b) -> mkProd(dn,t,b)
     | Lambda (_,t,b) -> mkLambda(dn,t,b)
     | LetIn (_,u,t,b) -> mkLetIn(dn,u,t,b)
-    | _ -> Term.map_constr canonize_binders c
+    | _ -> EConstr.map sigma canonize_binders c
   in
   canonize_binders c
 
@@ -118,8 +119,8 @@ let canonize_constr c =
 let display_eq ~flags env sigma t1 t2 =
   (* terms are canonized, then their externalisation is compared syntactically *)
   let open Constrextern in
-  let t1 = canonize_constr t1 in
-  let t2 = canonize_constr t2 in
+  let t1 = canonize_constr sigma t1 in
+  let t2 = canonize_constr sigma t2 in
   let ct1 = Flags.with_options flags (fun () -> extern_constr false env sigma t1) () in
   let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) () in
   Constrexpr_ops.constr_expr_eq ct1 ct2
@@ -129,7 +130,7 @@ let display_eq ~flags env sigma t1 t2 =
 let rec pr_explicit_aux env sigma t1 t2 = function
 | [] ->
   (** no specified flags: default. *)
-  (quote (Printer.pr_lconstr_env env sigma t1), quote (Printer.pr_lconstr_env env sigma t2))
+  (quote (Printer.pr_leconstr_env env sigma t1), quote (Printer.pr_leconstr_env env sigma t2))
 | flags :: rem ->
   let equal = display_eq ~flags env sigma t1 t2 in
   if equal then
@@ -153,7 +154,7 @@ let explicit_flags =
     [print_universes; print_implicits; print_coercions; print_no_symbol] (** and more! *) ]
 
 let pr_explicit env sigma t1 t2 =
-  pr_explicit_aux env sigma (EConstr.to_constr sigma t1) (EConstr.to_constr sigma t2) explicit_flags
+  pr_explicit_aux env sigma t1 t2 explicit_flags
 
 let pr_db env i =
   try