Canonisation de certains noms dans Pretyping, Asterm et Safe_typing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@586 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 113 insertions, 92 deletions

diff --git a/dev/changements.txt b/dev/changements.txt
index e54858016c..dc9b01b17b 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -83,6 +83,7 @@ Changements dans les fonctions :
 	Typing, Machops
 	  type_of_type     ->  judge_of_type
 	  fcn_proposition  ->  judge_of_prop_contents
+	  safe_fmachine    ->  safe_infer
 
 	Reduction, Clenv
           whd_betadeltat      -> whd_betaevar
@@ -93,7 +94,8 @@ Changements dans les fonctions :
           constr_of_com_sort   -> interp_type
           constr_of_com        -> interp_constr
           rawconstr_of_com     -> interp_rawconstr
-          type_of_com          -> typed_type_of_com
+          type_of_com          -> type_judgement_of_rawconstr
+	  judgement_of_com     -> judgement_of_rawconstr
 
         Termast
           bdize                -> ast_of_constr
@@ -134,9 +136,11 @@ Changements dans les fonctions :
         Declare
   	  machine_constant ->   declare_constant (+ modifs)
 
-	ex-Trad
+	ex-Trad, maintenant Pretyping
           inh_cast_rel        -> Coercion.inh_conv_coerce_to
           inh_conv_coerce_to  -> Coercion.inh_conv_coerce_to_fail
+	  ise_resolve1        -> ise_resolve, ise_resolve_type
+	  ise_resolve         -> ise_infer, ise_infer_type
 
 Changements dans les inductifs
 ------------------------------
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c99bd4bbbb..ca5d4a2ecc 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -167,11 +167,11 @@ let execute_type mf env constr =
    allowed (the flag [fix] is not set) and all verifications done (the
    flag [nocheck] is not set). *)
 
-let safe_machine env constr = 
+let safe_infer env constr = 
   let mf = { fix = false; nocheck = false } in
   execute mf env constr
 
-let safe_machine_type env constr = 
+let safe_infer_type env constr = 
   let mf = { fix = false; nocheck = false } in
   execute_type mf env constr
 
@@ -187,11 +187,11 @@ let fix_machine_type env constr =
 
 (* Fast machines without any verification. *)
 
-let unsafe_machine env constr = 
+let unsafe_infer env constr = 
   let mf = { fix = true; nocheck = true } in
   execute mf env constr
 
-let unsafe_machine_type env constr = 
+let unsafe_infer_type env constr = 
   let mf = { fix = true; nocheck = true } in
   execute_type mf env constr
 
@@ -199,30 +199,30 @@ let unsafe_machine_type env constr =
 (* ``Type of'' machines. *)
 
 let type_of env c = 
-  let (j,_) = safe_machine env c in nf_betaiota env Evd.empty (body_of_type j.uj_type)
+  let (j,_) = safe_infer env c in nf_betaiota env Evd.empty (body_of_type j.uj_type)
 
 (* obsolètes
 let type_of_type env c = 
-  let tt = safe_machine_type env c in DOP0 (Sort (level_of_type tt.typ)
+  let tt = safe_infer_type env c in DOP0 (Sort (level_of_type tt.typ)
 
 let unsafe_type_of env c = 
-  let (j,_) = unsafe_machine env c in nf_betaiota env Evd.empty j.uj_type
+  let (j,_) = unsafe_infer env c in nf_betaiota env Evd.empty j.uj_type
 
 let unsafe_type_of_type env c = 
-  let tt = unsafe_machine_type env c in DOP0 (Sort tt.typ)
+  let tt = unsafe_infer_type env c in DOP0 (Sort tt.typ)
 *)
 (* Typing of several terms. *)
 
-let safe_machine_l env cl =
+let safe_infer_l env cl =
   let type_one (cst,l) c =
-    let (j,cst') = safe_machine env c in
+    let (j,cst') = safe_infer env c in
     (Constraint.union cst cst', j::l)
   in
   List.fold_left type_one (Constraint.empty,[]) cl
 
-let safe_machine_v env cv =
+let safe_infer_v env cv =
   let type_one (cst,l) c =
-    let (j,cst') = safe_machine env c in
+    let (j,cst') = safe_infer env c in
     (Constraint.union cst cst', j::l)
   in
   let cst',l = Array.fold_left type_one (Constraint.empty,[]) cv in
@@ -250,7 +250,7 @@ let lookup_mind_specif = lookup_mind_specif
    being added to the environment. *)
 
 let push_rel_or_var_def push (id,c) env =
-  let (j,cst) = safe_machine env c in
+  let (j,cst) = safe_infer env c in
   let env' = add_constraints cst env in
   push (id,j.uj_val,j.uj_type) env'
 
@@ -259,7 +259,7 @@ let push_var_def nvar env = push_rel_or_var_def push_var_def nvar env
 let push_rel_def nrel env = push_rel_or_var_def push_rel_def nrel env
 
 let push_rel_or_var_decl push (id,c) env =
-  let (j,cst) = safe_machine_type env c in
+  let (j,cst) = safe_infer_type env c in
   let env' = add_constraints cst env in
   let var = assumption_of_type_judgment j in
   push (id,var) env'
@@ -274,14 +274,14 @@ let push_rels_with_univ vars env =
 (* Insertion of constants and parameters in environment. *)
 
 let add_constant_with_value sp body typ env =
-  let (jb,cst) = safe_machine env body in
+  let (jb,cst) = safe_infer env body in
   let env' = add_constraints cst env in
   let (env'',ty,cst') = 
     match typ with
       | None -> 
 	  env', typed_type_of_judgment env' Evd.empty jb, Constraint.empty
       | Some ty -> 
-	  let (jt,cst') = safe_machine env ty in
+	  let (jt,cst') = safe_infer env ty in
 	  let env'' = add_constraints cst' env' in
 	  try
 	    let cst'' = conv env'' Evd.empty (body_of_type jb.uj_type) jt.uj_val in
@@ -305,7 +305,7 @@ let add_constant_with_value sp body typ env =
   add_constant sp cb env''
 
 let add_lazy_constant sp f t env =
-  let (jt,cst) = safe_machine env t in
+  let (jt,cst) = safe_infer env t in
   let env' = add_constraints cst env in
   let ids = global_vars_set jt.uj_val in
   let cb = {
@@ -327,7 +327,7 @@ let add_constant sp ce env =
 	   | None -> error "you cannot declare a lazy constant without type")
 
 let add_parameter sp t env =
-  let (jt,cst) = safe_machine env t in
+  let (jt,cst) = safe_infer env t in
   let env' = add_constraints cst env in
   let ids = global_vars_set jt.uj_val in
   let cb = {
@@ -357,7 +357,7 @@ let max_universe (s1,cst1) (s2,cst2) g =
 let rec infos_and_sort env t =
   match kind_of_term t with
     | IsProd (name,c1,c2) ->
-        let (varj,_) = safe_machine_type env c1 in
+        let (varj,_) = safe_infer_type env c1 in
 	let var = assumption_of_type_judgment varj in
 	let env1 = Environ.push_rel_decl (name,var) env in
 	let s1 = varj.utj_type in
@@ -402,7 +402,7 @@ let type_one_constructor env_ar nparams arsort c =
     let env_par = push_rels params env_ar in
     infos_and_sort env_par dc in
   (* Constructors are typed-checked here *)
-  let (j,cst) = safe_machine_type env_ar c in
+  let (j,cst) = safe_infer_type env_ar c in
 
   (* If the arity is at some level Type arsort, then the sort of the
      constructor must be below arsort; here we consider constructors with the
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index c2fb4a3c09..577f753d37 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -61,21 +61,21 @@ val import : compiled_env -> safe_environment -> safe_environment
 val env_of_safe_env : safe_environment -> env
 
 
-(*s Typing judgments (only used in minicoq). *)
+(*s Typing judgments without modifying the global safe env - used in minicoq *)
 
 type judgment
 
 val j_val : judgment -> constr
 val j_type : judgment -> constr
 
-val safe_machine : safe_environment -> constr -> judgment * constraints
+val safe_infer : safe_environment -> constr -> judgment * constraints
 
 (*i For debug
 val fix_machine : safe_environment -> constr -> judgment * constraints
 val fix_machine_type : safe_environment -> constr -> typed_type * constraints
 
-val unsafe_machine : safe_environment -> constr -> judgment * constraints
-val unsafe_machine_type : safe_environment -> constr -> typed_type * constraints
+val unsafe_infer : safe_environment -> constr -> judgment * constraints
+val unsafe_infer_type : safe_environment -> constr -> typed_type * constraints
 
 val type_of : safe_environment -> constr -> constr
 
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 3b881b5169..853798daba 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -545,27 +545,21 @@ let _ =
 
 (* Endless^H^H^H^H^H^H^HShort list of alternative ways to call pretyping *)
 
-let interp_constr_gen is_ass sigma env com = 
-  let c = interp_rawconstr sigma env com in
-  try 
-    ise_resolve1 is_ass sigma env c
-  with e -> 
-    Stdpp.raise_with_loc (Ast.loc com) e
-
-let interp_constr sigma env c = interp_constr_gen false sigma env c
-let interp_type sigma env   c = interp_constr_gen true sigma env c
+let interp_constr sigma env c =
+  ise_resolve sigma env (interp_rawconstr sigma env c)
+let interp_type sigma env   c =
+  ise_resolve_type sigma env (interp_rawconstr sigma env c)
 let interp_sort = function
   | Node(loc,"PROP", []) -> Prop Null
   | Node(loc,"SET", [])  -> Prop Pos
   | Node(loc,"TYPE", []) -> Type Univ.dummy_univ
   | a -> user_err_loc (Ast.loc a,"interp_sort", [< 'sTR "Not a sort" >])
 
-let judgment_of_com sigma env com = 
-  let c = interp_rawconstr sigma env com in
-  try
-    ise_resolve false sigma [] env [] [] c
-  with e -> 
-    Stdpp.raise_with_loc (Ast.loc com) e
+let judgment_of_rawconstr sigma env c =
+  ise_infer sigma env (interp_rawconstr sigma env c)
+
+let type_judgment_of_rawconstr sigma env c =
+  ise_infer_type sigma env (interp_rawconstr sigma env c)
 
 (*To retype a list of key*constr with undefined key*)
 let retype_list sigma env lst=
@@ -583,13 +577,6 @@ let interp_constr1 sigma env lvar lmeta com =
   with e -> 
     Stdpp.raise_with_loc (Ast.loc com) e
 
-let typed_type_of_com sigma env com =
-  let c = interp_rawconstr sigma env com in
-  try 
-    ise_resolve_type true sigma [] env c
-  with e -> 
-    Stdpp.raise_with_loc (Ast.loc com) e
-
 (* Note: typ is retyped *)
 
 let interp_casted_constr sigma env com typ = 
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 285f997ceb..95810a36f0 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -17,11 +17,12 @@ val interp_rawconstr     : 'a evar_map -> env -> Coqast.t -> rawconstr
 val interp_constr        : 'a evar_map -> env -> Coqast.t -> constr
 val interp_casted_constr : 'a evar_map -> env -> Coqast.t -> constr -> constr
 val interp_type          : 'a evar_map -> env -> Coqast.t -> constr
-val typed_type_of_com    : 'a evar_map -> env -> Coqast.t -> typed_type
-val judgment_of_com      : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
-
 val interp_sort          : Coqast.t -> sorts
 
+val judgment_of_rawconstr : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
+val type_judgment_of_rawconstr :
+  'a evar_map -> env -> Coqast.t -> unsafe_type_judgment
+
 (*Interprets a constr according to two lists of instantiations (variables and
   metas)*)
 val interp_constr1     :
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 147960ade4..c2770f1961 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -465,14 +465,14 @@ and pretype_type valcon env isevars lvar lmeta = function
 	  error_unexpected_type_loc (loc_of_rawconstr c) env tj.uj_val v
 
 
-let unsafe_fmachine tycon nocheck isevars metamap env lvar lmeta constr =
+let unsafe_infer tycon nocheck isevars metamap env lvar lmeta constr =
   trad_metamap := metamap;
   trad_nocheck := nocheck;
   reset_problems ();
   pretype tycon env isevars lvar lmeta constr
 
 
-let unsafe_fmachine_type valcon nocheck isevars metamap env lvar lmeta constr =
+let unsafe_infer_type valcon nocheck isevars metamap env lvar lmeta constr =
   trad_metamap := metamap;
   trad_nocheck := nocheck;
   reset_problems ();
@@ -498,6 +498,13 @@ let j_apply f env sigma j =
   { uj_val=strong (under_outer_cast f) env sigma j.uj_val;
     uj_type= typed_app (strong f env sigma) j.uj_type }
 
+let utj_apply f env sigma j =
+  let under_outer_cast f env sigma = function
+    | DOP2 (Cast,b,t) -> DOP2 (Cast,f env sigma b,f env sigma t)
+    | c -> f env sigma c in
+  { utj_val = strong (under_outer_cast f) env sigma j.utj_val;
+    utj_type = j.utj_type }
+
 (* TODO: comment faire remonter l'information si le typage a resolu des
        variables du sigma original. il faudrait que la fonction de typage
        retourne aussi le nouveau sigma...
@@ -505,39 +512,45 @@ let j_apply f env sigma j =
 
 let ise_resolve_casted_gen fail_evar sigma env lvar lmeta typ c =
   let isevars = ref sigma in
-  let j = unsafe_fmachine (mk_tycon typ) false isevars [] env lvar lmeta c in
+  let j = unsafe_infer (mk_tycon typ) false isevars [] env lvar lmeta c in
   (j_apply (fun _ -> process_evars fail_evar) env !isevars j).uj_val
 
 let ise_resolve_casted sigma env typ c =
   ise_resolve_casted_gen true sigma env [] [] typ c
 
-(* Raw calls to the inference machine of Trad: boolean says if we must fail
+(* Raw calls to the unsafe inference machine: boolean says if we must fail
    on unresolved evars, or replace them by Metas; the unsafe_judgment list
    allows us to extend env with some bindings *)
-let ise_resolve fail_evar sigma metamap env lvar lmeta c =
+let ise_infer_gen fail_evar sigma metamap env lvar lmeta c =
   let isevars = ref sigma in
-  let j = unsafe_fmachine empty_tycon false isevars metamap env lvar lmeta c in
+  let j = unsafe_infer empty_tycon false isevars metamap env lvar lmeta c in
   j_apply (fun _ -> process_evars fail_evar) env !isevars j
 
-let ise_resolve_type fail_evar sigma metamap env c =
+let ise_infer_type_gen fail_evar sigma metamap env c =
   let isevars = ref sigma in
-  let j = unsafe_fmachine_type empty_valcon false isevars metamap env [] [] c in
-  let tj = assumption_of_type_judgment (inh_ass_of_j env isevars j) in
-  typed_app (strong (fun _ -> process_evars fail_evar) env !isevars) tj
+  let j = unsafe_infer_type empty_valcon false isevars metamap env [] [] c in
+  let tj = inh_ass_of_j env isevars j in
+  utj_apply (fun _ -> process_evars fail_evar) env !isevars tj
 
-let ise_resolve_nocheck sigma metamap env c =
+let ise_infer_nocheck sigma metamap env c =
   let isevars = ref sigma in
-  let j = unsafe_fmachine empty_tycon true isevars metamap env [] [] c in
+  let j = unsafe_infer empty_tycon true isevars metamap env [] [] c in
   j_apply (fun _ -> process_evars true) env !isevars j
 
-let ise_resolve1 is_ass sigma env c =
-  if is_ass then 
-    body_of_type (ise_resolve_type true sigma [] env c)
-  else 
-    (ise_resolve true sigma [] env [] [] c).uj_val
+let ise_infer sigma env c =
+  ise_infer_gen true sigma [] env [] [] c
+
+let ise_infer_type sigma env c =
+  ise_infer_type_gen true sigma [] env c
+
+let ise_resolve sigma env c =
+  (ise_infer_gen true sigma [] env [] [] c).uj_val
+
+let ise_resolve_type sigma env c =
+  (ise_infer_type_gen true sigma [] env c).utj_val
 
 let ise_resolve2 sigma env lmeta lvar c =
-  (ise_resolve true sigma [] env lmeta lvar c).uj_val;;
+  (ise_infer_gen true sigma [] env lmeta lvar c).uj_val;;
 
 (* Keeping universe constraints *)
 (*
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index eb72b7e00d..099f75140a 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -14,16 +14,24 @@ open Evarutil
 (* Raw calls to the inference machine of Trad: boolean says if we must fail
    on unresolved evars, or replace them by Metas ; the [unsafe_judgment] list
    allows us to extend env with some bindings *)
-val ise_resolve : bool -> 'a evar_map -> (int * constr) list ->
+val ise_infer_gen : bool -> 'a evar_map -> (int * constr) list ->
   env -> (identifier * unsafe_judgment) list ->
   (int * unsafe_judgment) list -> rawconstr -> unsafe_judgment
 
-val ise_resolve_type : bool -> 'a evar_map -> (int * constr) list ->
-  env -> rawconstr -> typed_type
+(* Standard call to get an unsafe judgment from a rawconstr, resolving
+   implicit args *)
+val ise_infer : 'a evar_map -> env -> rawconstr -> unsafe_judgment
+
+(* Standard call to get an unsafe type judgment from a rawconstr, resolving
+   implicit args *)
+val ise_infer_type : 'a evar_map -> env -> rawconstr -> unsafe_type_judgment
+
+(* Standard call to get a constr from a rawconstr, resolving implicit args *)
+val ise_resolve      : 'a evar_map -> env -> rawconstr -> constr
+
+(* Idem but the rawconstr is intended to be a type *)
+val ise_resolve_type : 'a evar_map -> env -> rawconstr -> constr
 
-(* Call [ise_resolve] with empty metamap and [fail_evar=true]. The boolean says
- * if we must coerce to a type *)
-val ise_resolve1 : bool -> 'a evar_map -> env -> rawconstr -> constr
 val ise_resolve2 : 'a evar_map -> env -> (identifier * unsafe_judgment) list ->
   (int * unsafe_judgment) list -> rawconstr -> constr
 
@@ -35,7 +43,7 @@ val ise_resolve_casted : 'a evar_map -> env -> constr -> rawconstr -> constr
 (* progmach.ml tries to type ill-typed terms: does not perform the conversion
  * test in application.
  *)
-val ise_resolve_nocheck : 'a evar_map -> (int * constr) list ->
+val ise_infer_nocheck : 'a evar_map -> (int * constr) list ->
   env -> rawconstr -> unsafe_judgment
 
 (* Typing with Trad, and re-checking with Mach *)
@@ -64,8 +72,8 @@ val infconstruct_type_with_univ_sp :
 i*)
 
 (*i*)
-(* Internal of Trad...
- * Unused outside Trad, but useful for debugging
+(* Internal of Pretyping...
+ * Unused outside, but useful for debugging
  *)
 val pretype : 
   type_constraint -> env -> 'a evar_defs ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 60d9e5f13a..7da510029f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -8,6 +8,7 @@ open Generic
 open Term
 open Declarations
 open Inductive
+open Environ
 open Reduction
 open Tacred
 open Declare
@@ -144,8 +145,9 @@ let build_mutual lparams lnamearconstrs finite =
     let (ind_env,arityl) =
       List.fold_left 
 	(fun (env,arl) (recname,arityc,_) -> 
-           let arity =
-	     typed_type_of_com Evd.empty env (mkProdCit lparams arityc) in
+           let raw_arity = mkProdCit lparams arityc in
+           let arj = type_judgment_of_rawconstr Evd.empty env raw_arity in
+	   let arity = Typeops.assumption_of_type_judgment arj in
 	   let env' = Environ.push_rel_decl (Name recname,arity) env in
 	   (env', (arity::arl)))
 	(env0,[]) lnamearconstrs 
@@ -218,8 +220,11 @@ let build_recursive lnameargsardef =
     try 
       List.fold_left 
         (fun (env,arl) (recname,lparams,arityc,_) -> 
-           let arity = typed_type_of_com Evd.empty env (mkProdCit lparams arityc) in
-           declare_variable recname (SectionLocalDecl (body_of_type arity),NeverDischarge,false);
+           let raw_arity = mkProdCit lparams arityc in
+           let arj = type_judgment_of_rawconstr Evd.empty env raw_arity in
+	   let arity = Typeops.assumption_of_type_judgment arj in
+           declare_variable recname
+	     (SectionLocalDecl arj.utj_val,NeverDischarge,false);
            (Environ.push_var_decl (recname,arity) env, (arity::arl)))
         (env0,[]) lnameargsardef
     with e ->
@@ -281,8 +286,10 @@ let build_corecursive lnameardef =
     try 
       List.fold_left 
         (fun (env,arl) (recname,arityc,_) -> 
-           let arity = typed_type_of_com Evd.empty env0 arityc in
-           declare_variable recname (SectionLocalDecl (body_of_type arity),NeverDischarge,false);
+           let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in
+	   let arity = Typeops.assumption_of_type_judgment arj in
+           declare_variable recname
+	     (SectionLocalDecl arj.utj_val,NeverDischarge,false);
            (Environ.push_var_decl (recname,arity) env, (arity::arl)))
         (env0,[]) lnameardef
     with e -> 
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 5df900c264..945ff63ef2 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -44,7 +44,7 @@ let rec globalize bv = function
 
 let check c = 
   let c = globalize [] c in
-  let (j,u) = safe_machine !env c in
+  let (j,u) = safe_infer !env c in
   let ty = j_type j in
   let pty = pr_term CCI (env_of_safe_env !env) ty in
   mSGNL (hOV 0 [< 'sTR"  :"; 'sPC; hOV 0 pty; 'fNL >])
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 0fc6f85a8b..9801045a2e 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -71,15 +71,17 @@ let typecheck_params_and_field ps fs =
   let env1,newps =
     List.fold_left
       (fun (env,newps) (id,t) -> 
-         let tj = typed_type_of_com Evd.empty env t in
-         (Environ.push_var_decl (id,tj) env,(id,body_of_type tj)::newps))
+         let tj = type_judgment_of_rawconstr Evd.empty env t in
+	 let ass = Typeops.assumption_of_type_judgment tj in
+         (Environ.push_var_decl (id,ass) env,(id,tj.Environ.utj_val)::newps))
       (env0,[]) ps
   in
   let env2,newfs =
     List.fold_left
       (fun (env,newfs) (id,t) -> 
-         let tj = typed_type_of_com Evd.empty env t in
-         (Environ.push_var_decl (id,tj) env,(id,body_of_type tj)::newfs)) (env1,[]) fs
+         let tj = type_judgment_of_rawconstr Evd.empty env t in
+	 let ass = Typeops.assumption_of_type_judgment tj in
+         (Environ.push_var_decl (id,ass) env,(id,tj.Environ.utj_val)::newfs)) (env1,[]) fs
   in
   List.rev(newps),List.rev(newfs)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 32a30d144c..4010c83599 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -813,7 +813,7 @@ let _ =
        | VARG_TACTIC_ARG (Redexp redexp) :: VARG_CONSTR c :: g ->
            let (evmap,sign) = get_current_context_of_args g in
            let redfun = print_eval (reduction_of_redexp redexp) sign in 
-	   fun () -> mSG (redfun (judgment_of_com evmap sign c))
+	   fun () -> mSG (redfun (judgment_of_rawconstr evmap sign c))
        | _ -> bad_vernac_args "Eval")
 
 let _ =
@@ -825,8 +825,7 @@ let _ =
 	     | "CHECK" -> print_val
              | "PRINTTYPE" -> print_type
              | _ -> anomaly "Unexpected string" 
-	   in
-	   (fun () -> mSG (prfun sign (judgment_of_com evmap sign c)))
+	   in (fun () -> mSG (prfun sign (judgment_of_rawconstr evmap sign c)))
        | _ -> bad_vernac_args "Check")
 
 (***