Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.

12 files changed, 55 insertions, 47 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 22881c32c..7159614d9 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -352,9 +352,9 @@ let raw_push_named (na,raw_value,raw_typ) env =
         let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
         (match raw_value with
         | None ->
-           Environ.push_named (NamedDecl.LocalAssum (id,typ)) env
+           EConstr.push_named (NamedDecl.LocalAssum (id,typ)) env
         | Some value ->
-           Environ.push_named (NamedDecl.LocalDef (id, value, typ)) env)
+           EConstr.push_named (NamedDecl.LocalDef (id, value, typ)) env)
 
 
 let add_pat_variables pat typ env : Environ.env =
@@ -519,7 +519,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 		   The "value" of this branch is then simply [res]
 		*)
 		let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
-		let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in
+                let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in
 		let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in
 		let res = fresh_id args_res.to_avoid "_res" in
 		let new_avoid = res::args_res.to_avoid in
@@ -631,12 +631,11 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
         let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (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
-	let v_type = EConstr.Unsafe.to_constr v_type in
+        let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
 	let new_env =
 	  match n with
 	      Anonymous -> env
-	    | Name id -> Environ.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env
+            | Name id -> EConstr.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env
 	in
 	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_letin n) v_res b_res
@@ -648,7 +647,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	build_entry_lc_from_case env funnames make_discr el brl avoid
     | GIf(b,(na,e_option),lhs,rhs) ->
 	let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
-	let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in
+        let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
 	let (ind,_) =
 	  try Inductiveops.find_inductive env (Evd.from_env env) b_typ
 	  with Not_found ->
@@ -680,7 +679,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	      nal
 	  in
 	  let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
-	  let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in
+          let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
 	  let (ind,_) =
 	    try Inductiveops.find_inductive env (Evd.from_env env) b_typ
 	    with Not_found ->
@@ -726,7 +725,7 @@ and build_entry_lc_from_case env funname make_discr
 	let types =
 	  List.map (fun (case_arg,_) ->
 		      let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in
-		      EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr case_arg_as_constr))
+                      EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr)
 		   ) el
 	in
 	(****** The next works only if the match is not dependent ****)
@@ -948,7 +947,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			  mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt])
 			in
 			let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
-			let new_env = Environ.push_rel (LocalAssum (n,t')) env in
+                        let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
 			let new_b,id_to_exclude =
 			  rebuild_cons new_env
 			    nb_args relname
@@ -983,7 +982,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    let subst_b =
 		      if is_in_b then b else  replace_var_by_term id rt b
 		    in
-		    let new_env = Environ.push_rel (LocalAssum (n,t')) env in
+                    let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
 		    let new_b,id_to_exclude =
 		      rebuild_cons
 			new_env
@@ -995,7 +994,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  with Continue ->
 		    let jmeq = Globnames.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in
 		    let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in
-		    let ind,args' = Inductive.find_inductive env ty' in
+                    let ind,args' = Inductiveops.find_inductive env Evd.(from_env env) ty' in
 		    let mib,_ = Global.lookup_inductive (fst ind) in
 		    let nparam = mib.Declarations.mind_nparams in
 		    let params,arg' =
@@ -1017,14 +1016,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
                     observe (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq');
 		    let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
 		    observe (str " computing new type for jmeq : done") ;
+                    let sigma = Evd.(from_env env) in
 		    let new_args =
-		      match Constr.kind eq'_as_constr with
+                      match EConstr.kind sigma eq'_as_constr with
 			| App(_,[|_;_;ty;_|]) ->
-			    let ty = Array.to_list (snd (destApp ty)) in
+                            let ty = Array.to_list (snd (EConstr.destApp sigma ty)) in
 			    let ty' = snd (Util.List.chop nparam ty) in
 			    List.fold_left2
 			      (fun acc var_as_constr arg ->
-                                let arg = EConstr.of_constr arg in
 				 if isRel var_as_constr
 				 then
 				   let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in
@@ -1065,7 +1064,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    in
 		    let new_env =
 		      let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in
-		      Environ.push_rel (LocalAssum (n,t')) env
+                      EConstr.push_rel (LocalAssum (n,t')) env
 		    in
 		    let new_b,id_to_exclude =
 		      rebuild_cons
@@ -1103,7 +1102,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      with Continue -> 
                 observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
 		let t',ctx = Pretyping.understand env (Evd.from_env env) t in
-		let new_env = Environ.push_rel (LocalAssum (n,t')) env in
+                let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
 		let new_b,id_to_exclude =
 		  rebuild_cons new_env
 		    nb_args relname
@@ -1119,7 +1118,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	    | _ ->
                 observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
 		let t',ctx = Pretyping.understand env (Evd.from_env env) t in
-		let new_env = Environ.push_rel (LocalAssum (n,t')) env in
+                let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
 		let new_b,id_to_exclude =
 		  rebuild_cons new_env
 		    nb_args relname
@@ -1140,7 +1139,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  let t',ctx = Pretyping.understand env (Evd.from_env env) t in
 	  match n with
 	    | Name id ->
-		let new_env = Environ.push_rel (LocalAssum (n,t')) env in
+                let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
 		let new_b,id_to_exclude =
 		  rebuild_cons new_env
 		    nb_args relname
@@ -1163,7 +1162,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  let evd = (Evd.from_env env) in
 	  let t',ctx = Pretyping.understand env evd t in
 	  let evd = Evd.from_ctx ctx in
-	  let type_t' = Typing.unsafe_type_of env evd (EConstr.of_constr t') in
+          let type_t' = Typing.unsafe_type_of env evd t' in
+          let t' = EConstr.Unsafe.to_constr t' in
 	  let type_t' = EConstr.Unsafe.to_constr type_t' in
 	  let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in
 	  let new_b,id_to_exclude =
@@ -1189,7 +1189,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      depth t
 	  in
 	  let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
-	  let new_env = Environ.push_rel (LocalAssum (na,t')) env in
+          let new_env = EConstr.push_rel (LocalAssum (na,t')) env in
 	  let new_b,id_to_exclude =
 	    rebuild_cons new_env
 	      nb_args relname
@@ -1369,8 +1369,9 @@ let do_build_inductive
     *)
     let rel_arities = Array.mapi rel_arity funsargs in
     Util.Array.fold_left2 (fun env rel_name rel_ar ->
-			     Environ.push_named (LocalAssum (rel_name,
-						             fst (with_full_print (Constrintern.interp_constr env evd) rel_ar))) env) env relnames rel_arities
+        let rex = fst (with_full_print (Constrintern.interp_constr env evd) rel_ar) in
+        let rex = EConstr.Unsafe.to_constr rex in
+        Environ.push_named (LocalAssum (rel_name,rex)) env) env relnames rel_arities
   in
   (* and of the real constructors*)
   let constr i res =
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e19fc9b62..13eda3952 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -141,8 +141,7 @@ let rec abstract_glob_constr c = function
   | Constrexpr.CLocalPattern _::bl -> assert false
 
 let interp_casted_constr_with_implicits env sigma impls c  =
-  Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
-    c
+  Constrintern.intern_gen Pretyping.WithoutTypeConstraint env sigma ~impls c
 
 (*
    Construct a fixpoint as a Glob_term
@@ -160,9 +159,9 @@ let build_newrecursive
         let arity,ctx = Constrintern.interp_type env0 sigma arityc in
         let evd = Evd.from_env env0 in
         let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in
-	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in
+        let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in
         let open Context.Named.Declaration in
-        (Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls))
+        (EConstr.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls))
       (env0,Constrintern.empty_internalization_env) lnameargsardef in
   let recdef =
     (* Declare local notations *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 8fe05b497..e2d7de6d5 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -210,6 +210,7 @@ let (value_f: Constr.t list -> global_reference -> Constr.t) =
 	    DAst.make @@ GVar v_id)])
     in
     let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in
+    let body = EConstr.Unsafe.to_constr body in
     it_mkLambda_or_LetIn body context
 
 let (declare_f : Id.t -> logical_kind -> Constr.t list -> global_reference -> global_reference) =
@@ -1400,7 +1401,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 	 	     (fun c ->
 	 		Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST 
 	 		  [intros;
-	 		   Simple.apply (EConstr.of_constr (fst (interp_constr (Global.env()) Evd.empty c))) (*FIXME*);
+                           Simple.apply (fst (interp_constr (Global.env()) Evd.empty c)) (*FIXME*);
 	 		   Tacticals.New.tclCOMPLETE Auto.default_auto
 	 		  ])
 	 	     )
@@ -1599,7 +1600,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       and functional_ref = destConst (constr_of_global functional_ref)
       and eq_ref = destConst (constr_of_global eq_ref) in
       generate_induction_principle f_ref tcc_lemma_constr
-        functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evd (EConstr.of_constr res)) (EConstr.of_constr relation);
+        functional_ref eq_ref rec_arg_num
+        (EConstr.of_constr rec_arg_type)
+        (nb_prod evd (EConstr.of_constr res)) relation;
       Flags.if_verbose
         msgnl (h 1 (Ppconstr.pr_id function_name ++
 			 spc () ++ str"is defined" )++ fnl () ++
@@ -1614,7 +1617,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       tcc_lemma_constr
       is_mes functional_ref
       (EConstr.of_constr rec_arg_type)
-      (EConstr.of_constr relation) rec_arg_num
+      relation rec_arg_num
       term_id
       using_lemmas
       (List.length res_vars)
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index b61611145..6c42518b1 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -253,6 +253,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
   let sigma = Evd.from_env env in
   let f ce =
     let c, ctx = Constrintern.interp_constr env sigma ce in
+    let c = EConstr.to_constr sigma c in
     let ctx =
       let ctx = UState.context_set ctx in
         if poly then ctx
@@ -554,6 +555,7 @@ let add_transitivity_lemma left lem =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let lem',ctx (*FIXME*) = Constrintern.interp_constr env sigma lem in
+  let lem' = EConstr.to_constr sigma lem' in
   add_anonymous_leaf (inTransitivity (left,lem'))
 
 (* Vernacular syntax *)
@@ -611,8 +613,10 @@ END
 
 VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF
  | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] ->
-           [ let tc,ctx = Constrintern.interp_constr (Global.env ()) Evd.empty c in
-             let tb,ctx(*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty b in
+           [ let tc,_ctx = Constrintern.interp_constr (Global.env ()) Evd.empty c in
+             let tb,_ctx(*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty b in
+             let tc = EConstr.to_constr Evd.empty tc in
+             let tb = EConstr.to_constr Evd.empty tb in
              Global.register f tc tb ]
 END
 
@@ -705,7 +709,6 @@ let hResolve id c occ t =
           resolve_hole (subst_hole_with_term loc_begin c_raw t_hole)
   in
   let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in
-  let t_constr = EConstr.of_constr t_constr in
   let sigma = Evd.merge_universe_context sigma ctx in
   let t_constr_type = Retyping.get_type_of env sigma t_constr in
   Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index d42259f2b..1f2189015 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1897,7 +1897,6 @@ let declare_projection n instance_id r =
 
 let build_morphism_signature env sigma m =
   let m,ctx = Constrintern.interp_constr env sigma m in
-  let m = EConstr.of_constr m in
   let sigma = Evd.from_ctx ctx in
   let t = Typing.unsafe_type_of env sigma m in
   let cstrs =
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 22ec6c5b1..9a10fb805 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -199,7 +199,7 @@ let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c =
     ltac_extra = extra;
   } in
   let c' =
-    warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env) c
+    warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env Evd.(from_env env)) c
   in
   (c',if !strict_check then None else Some c)
 
@@ -316,7 +316,7 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc =
     ltac_extra = ist.extra;
   } in
   let metas,pat = Constrintern.intern_constr_pattern
-    ist.genv ~as_type ~ltacvars pc
+    ist.genv Evd.(from_env ist.genv) ~as_type ~ltacvars pc
   in
   let (glob,_ as c) = intern_constr_gen true false ist pc in
   let bound_names = Glob_ops.bound_glob_vars glob in
@@ -335,7 +335,7 @@ let intern_typed_pattern ist ~as_type ~ltacvars p =
           ltac_bound = Id.Set.empty;
           ltac_extra = ist.extra;
         } in
-      Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars p
+      Constrintern.intern_constr_pattern ist.genv Evd.(from_env ist.genv) ~as_type ~ltacvars p
     else
       [], dummy_pat in
   let (glob,_ as c) = intern_constr_gen true false ist p in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 79b5c1622..6a04badf3 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -584,7 +584,7 @@ let interp_glob_closure ist env sigma ?(kind=WithoutTypeConstraint) ?(pattern_mo
         ltac_bound = Id.Map.domain ist.lfun;
         ltac_extra = Genintern.Store.empty;
       } in
-      { closure ; term = intern_gen kind ~pattern_mode ~ltacvars env term_expr }
+      { closure ; term = intern_gen kind ~pattern_mode ~ltacvars env sigma term_expr }
 
 let interp_uconstr ist env sigma c = interp_glob_closure ist env sigma c
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 125afb1a0..0f0dbfff3 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -148,7 +148,7 @@ let ic c =
 let ic_unsafe c = (*FIXME remove *)
   let env = Global.env() in
   let sigma = Evd.from_env env in
-    EConstr.of_constr (fst (Constrintern.interp_constr env sigma c))
+  fst (Constrintern.interp_constr env sigma c)
 
 let decl_constant na univs c =
   let open Constr in
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 4ae746288..1a02fb91c 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -203,7 +203,7 @@ let glob_constr ist genv = function
     let vars = Id.Map.fold (fun x _ accu -> Id.Set.add x accu) ist.Tacinterp.lfun Id.Set.empty in
     let ltacvars = {
       Constrintern.empty_ltac_sign with Constrintern.ltac_vars = vars } in
-    Constrintern.intern_gen Pretyping.WithoutTypeConstraint ~ltacvars genv ce
+    Constrintern.intern_gen Pretyping.WithoutTypeConstraint ~ltacvars genv Evd.(from_env genv) ce
   | rc, None -> rc
 
 let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 8e6e0347f..96ded5abf 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -335,7 +335,8 @@ let push_rels_assum l e =
   push_rels_assum l e
 
 let coerce_search_pattern_to_sort hpat =
-  let env = Global.env () and sigma = Evd.empty in
+  let env = Global.env () in
+  let sigma = Evd.(from_env env) in
   let mkPApp fp n_imps args =
     let args' = Array.append (Array.make n_imps (Pattern.PMeta None)) args in
     Pattern.PApp (fp, args') in
@@ -393,8 +394,9 @@ let interp_search_arg arg =
       interp_search_notation ~loc s key
   | RGlobSearchSubPattern p ->
       try
-        let intern = Constrintern.intern_constr_pattern in 
-        Search.GlobSearchSubPattern (snd (intern (Global.env()) p))
+        let env = Global.env () in
+        let _, p = Constrintern.intern_constr_pattern env (Evd.from_env env) p in
+        Search.GlobSearchSubPattern p
       with e -> let e = CErrors.push e in iraise (ExplainErr.process_vernac_interp_error e)) arg in
   let hpat, a1 = match arg with
   | (_, Search.GlobSearchSubPattern (Pattern.PMeta _)) :: a' -> all_true, a'
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 61b65e347..f2990070b 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -55,7 +55,8 @@ let in_viewhint =
        Libobject.classify_function = classify_viewhint }
 
 let glob_view_hints lvh =
-  List.map (Constrintern.intern_constr (Global.env ())) lvh
+  let env = Global.env () in
+  List.map (Constrintern.intern_constr env Evd.(from_env env)) lvh
 
 let add_view_hints lvh i = Lib.add_anonymous_leaf (in_viewhint (i, lvh))
 
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 73e212365..d05f50e6d 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -73,11 +73,11 @@ let env_size env = List.length (Environ.named_context env)
 let safeDestApp c =
   match kind c with App (f, a) -> f, a | _ -> c, [| |]
 (* Toplevel constr must be globalized twice ! *)
-let glob_constr ist genv = function
+let glob_constr ist genv sigma = function
   | _, Some ce ->
     let vars = Id.Map.fold (fun x _ accu -> Id.Set.add x accu) ist.lfun Id.Set.empty in
     let ltacvars = { Constrintern.empty_ltac_sign with Constrintern.ltac_vars = vars } in
-    Constrintern.intern_gen WithoutTypeConstraint ~ltacvars:ltacvars genv ce
+    Constrintern.intern_gen WithoutTypeConstraint ~ltacvars:ltacvars genv sigma ce
   | rc, None -> rc
 
 (* Term printing utilities functions for deciding bracketing.  *)
@@ -1009,7 +1009,7 @@ let interp_wit wit ist gl x =
   sigma, Value.cast (topwit wit) arg
 let interp_open_constr ist gl gc =
   interp_wit wit_open_constr ist gl gc
-let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c
+let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) gl.sigma c
 let interp_term ist gl (_, c) = on_snd EConstr.Unsafe.to_constr (interp_open_constr ist gl c)
 let pr_ssrterm _ _ _ = pr_term
 let input_ssrtermkind strm = match stream_nth 0 strm with