aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/ide_slave.ml1
-rw-r--r--ltac/rewrite.ml9
-rw-r--r--ltac/tacinterp.ml8
-rw-r--r--plugins/decl_mode/g_decl_mode.ml42
-rw-r--r--plugins/setoid_ring/newring.ml2
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--printing/prettyp.ml15
-rw-r--r--printing/prettyp.mli8
-rw-r--r--printing/printer.ml12
-rw-r--r--printing/printer.mli9
-rw-r--r--tactics/class_tactics.ml9
-rw-r--r--tactics/hints.ml8
-rw-r--r--tactics/leminv.ml8
-rw-r--r--tactics/tactics.ml2
-rw-r--r--toplevel/himsg.ml70
-rw-r--r--toplevel/vernacentries.ml11
16 files changed, 81 insertions, 95 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index c11c78587..fcba01353 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -192,6 +192,7 @@ let process_goal sigma g =
let id = Goal.uid g in
let ccl =
let norm_constr = Reductionops.nf_evar sigma (EConstr.Unsafe.to_constr (Goal.V82.concl sigma g)) in
+ let norm_constr = EConstr.of_constr norm_constr in
Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr)
in
let process_hyp d (env,l) =
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 85c19fac4..3c6bd4563 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1526,7 +1526,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
| Success res ->
let (_, cstrs) = res.rew_evars in
let evars' = solve_constraints env res.rew_evars in
- let newt = EConstr.of_constr (Evarutil.nf_evar evars' (EConstr.Unsafe.to_constr res.rew_to)) in
+ let newt = nf_evar evars' res.rew_to in
let evars = (* Keep only original evars (potentially instantiated) and goal evars,
the rest has been defined and substituted already. *)
Evar.Set.fold
@@ -2151,10 +2151,9 @@ let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite
(** [setoid_]{reflexivity,symmetry,transitivity} tactics *)
-let not_declared env ty rel =
- let rel = EConstr.Unsafe.to_constr rel in
+let not_declared env sigma ty rel =
tclFAIL 0
- (str" The relation " ++ Printer.pr_constr_env env Evd.empty rel ++ str" is not a declared " ++
+ (str" The relation " ++ Printer.pr_econstr_env env sigma rel ++ str" is not a declared " ++
str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library")
let setoid_proof ty fn fallback =
@@ -2181,7 +2180,7 @@ let setoid_proof ty fn fallback =
begin match e with
| (Not_found, _) ->
let rel, _, _ = decompose_app_rel env sigma concl in
- not_declared env ty rel
+ not_declared env sigma ty rel
| (e, info) -> Proofview.tclZERO ~info e
end
| e' -> Proofview.tclZERO ~info e'
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 1fe6dbdd0..d8df07733 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -858,14 +858,16 @@ let rec message_of_value v =
Ftactic.return (int (out_gen (topwit wit_int) v))
else if has_type v (topwit wit_intro_pattern) then
let p = out_gen (topwit wit_intro_pattern) v in
- let print env sigma c = pr_constr_env env sigma (EConstr.Unsafe.to_constr (fst (Tactics.run_delayed env Evd.empty c))) in
+ let print env sigma c =
+ let (c, sigma) = Tactics.run_delayed env sigma c in
+ pr_econstr_env env sigma c
+ in
Ftactic.nf_enter { enter = begin fun gl ->
Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p)
end }
else if has_type v (topwit wit_constr_context) then
let c = out_gen (topwit wit_constr_context) v in
- let c = EConstr.Unsafe.to_constr c in
- Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (project gl) c) end }
+ Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end }
else if has_type v (topwit wit_uconstr) then
let c = out_gen (topwit wit_uconstr) v in
Ftactic.nf_enter { enter = begin fun gl ->
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 9e2c9f597..18a35c6cf 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -25,7 +25,7 @@ open Ppdecl_proof
let pr_goal gs =
let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in
let env = Goal.V82.env sigma g in
- let concl = EConstr.Unsafe.to_constr (Goal.V82.concl sigma g) in
+ let concl = Goal.V82.concl sigma g in
let goal =
Printer.pr_context_of env sigma ++ cut () ++
str "============================" ++ cut () ++
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index ce2c558ae..358ea5685 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -343,7 +343,7 @@ let _ = add_map "ring"
(****************************************************************************)
(* Ring database *)
-let pr_constr c = pr_constr (EConstr.Unsafe.to_constr c)
+let pr_constr c = pr_econstr c
module Cmap = Map.Make(Constr)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index afb0bf6d5..87267d538 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -385,7 +385,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
match is_unification_pattern_evar env evd ev lF tM with
| None -> fallback ()
| Some l1' -> (* Miller-Pfenning's patterns unification *)
- let t2 = EConstr.of_constr (nf_evar evd (EConstr.Unsafe.to_constr tM)) (** FIXME *) in
+ let t2 = tM in
let t2 = solve_pattern_eqn env evd l1' t2 in
solve_simple_eqn (evar_conv_x ts) env evd
(position_problem on_left pbty,ev,t2)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index e2c0f55f8..93970512d 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -42,8 +42,8 @@ type object_pr = {
print_named_decl : Context.Named.Declaration.t -> std_ppcmds;
print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option;
print_context : bool -> int option -> Lib.library_segment -> std_ppcmds;
- print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds;
- print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds;
+ print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.std_ppcmds;
+ print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds;
}
let gallina_print_module = print_module
@@ -433,8 +433,8 @@ let print_located_qualid ref = print_located_qualid "object" [`TERM; `LTAC; `MOD
(**** Gallina layer *****)
let gallina_print_typed_value_in_env env sigma (trm,typ) =
- (pr_lconstr_env env sigma trm ++ fnl () ++
- str " : " ++ pr_ltype_env env sigma typ)
+ (pr_leconstr_env env sigma trm ++ fnl () ++
+ str " : " ++ pr_letype_env env sigma typ)
(* To be improved; the type should be used to provide the types in the
abstractions. This should be done recursively inside pr_lconstr, so that
@@ -595,8 +595,7 @@ let gallina_print_context with_values =
prec
let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} =
- let ntrm = red_fun env sigma (EConstr.of_constr trm) in
- let ntrm = EConstr.Unsafe.to_constr ntrm in
+ let ntrm = red_fun env sigma trm in
(str " = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ))
(******************************************)
@@ -643,6 +642,8 @@ let print_judgment env sigma {uj_val=trm;uj_type=typ} =
let print_safe_judgment env sigma j =
let trm = Safe_typing.j_val j in
let typ = Safe_typing.j_type j in
+ let trm = EConstr.of_constr trm in
+ let typ = EConstr.of_constr typ in
print_typed_value_in_env env sigma (trm, typ)
(*********************)
@@ -762,7 +763,9 @@ let print_opaque_name qid =
| IndRef (sp,_) ->
print_inductive sp
| ConstructRef cstr as gr ->
+ let open EConstr in
let ty = Universes.unsafe_type_of_global gr in
+ let ty = EConstr.of_constr ty in
print_typed_value (mkConstruct cstr, ty)
| VarRef id ->
env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 0eab15579..38e111034 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -27,11 +27,11 @@ val print_full_context_typ : unit -> std_ppcmds
val print_full_pure_context : unit -> std_ppcmds
val print_sec_context : reference -> std_ppcmds
val print_sec_context_typ : reference -> std_ppcmds
-val print_judgment : env -> Evd.evar_map -> unsafe_judgment -> std_ppcmds
+val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> std_ppcmds
val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> std_ppcmds
val print_eval :
reduction_function -> env -> Evd.evar_map ->
- Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds
+ Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds
val print_name : reference or_by_notation -> std_ppcmds
val print_opaque_name : reference -> std_ppcmds
@@ -69,8 +69,8 @@ type object_pr = {
print_named_decl : Context.Named.Declaration.t -> std_ppcmds;
print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option;
print_context : bool -> int option -> Lib.library_segment -> std_ppcmds;
- print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds;
- print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds
+ print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.std_ppcmds;
+ print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds
}
val set_object_pr : object_pr -> unit
diff --git a/printing/printer.ml b/printing/printer.ml
index 4a6c83bd7..ba4b68296 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -99,7 +99,6 @@ let pr_type_core goal_concl_style env sigma t =
let pr_ltype_core goal_concl_style env sigma t =
pr_lconstr_expr (extern_type goal_concl_style env sigma t)
-let pr_goal_concl_style_env env = pr_ltype_core true env
let pr_ltype_env env = pr_ltype_core false env
let pr_type_env env = pr_type_core false env
@@ -110,8 +109,13 @@ 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_ljudge_env env sigma j =
- (pr_lconstr_env env sigma j.uj_val, pr_lconstr_env env sigma j.uj_type)
+ (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type)
let pr_ljudge j =
let (sigma, env) = get_current_context () in
@@ -390,7 +394,7 @@ let pr_transparent_state (ids, csts) =
let default_pr_goal gs =
let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in
let env = Goal.V82.env sigma g in
- let concl = EConstr.Unsafe.to_constr (Goal.V82.concl sigma g) in
+ let concl = Goal.V82.concl sigma g in
let goal =
pr_context_of env sigma ++ cut () ++
str "============================" ++ cut () ++
@@ -413,7 +417,7 @@ let pr_goal_name sigma g =
let pr_concl n sigma g =
let (g,sigma) = Goal.V82.nf_evar sigma g in
let env = Goal.V82.env sigma g in
- let pc = pr_goal_concl_style_env env sigma (EConstr.Unsafe.to_constr (Goal.V82.concl sigma g)) in
+ let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in
str (emacs_str "") ++
str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g ++
str " is:" ++ cut () ++ str" " ++ pc
diff --git a/printing/printer.mli b/printing/printer.mli
index 7521468e2..504392e35 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -43,6 +43,9 @@ val pr_econstr : EConstr.t -> std_ppcmds
val pr_leconstr_env : env -> evar_map -> EConstr.t -> std_ppcmds
val pr_leconstr : EConstr.t -> std_ppcmds
+val pr_etype_env : env -> evar_map -> EConstr.types -> std_ppcmds
+val pr_letype_env : env -> evar_map -> EConstr.types -> std_ppcmds
+
val pr_open_constr_env : env -> evar_map -> open_constr -> std_ppcmds
val pr_open_constr : open_constr -> std_ppcmds
@@ -55,7 +58,7 @@ val pr_constr_under_binders : constr_under_binders -> std_ppcmds
val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> std_ppcmds
val pr_lconstr_under_binders : constr_under_binders -> std_ppcmds
-val pr_goal_concl_style_env : env -> evar_map -> types -> std_ppcmds
+val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> std_ppcmds
val pr_ltype_env : env -> evar_map -> types -> std_ppcmds
val pr_ltype : types -> std_ppcmds
@@ -65,8 +68,8 @@ val pr_type : types -> std_ppcmds
val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> std_ppcmds
val pr_closed_glob : closed_glob_constr -> std_ppcmds
-val pr_ljudge_env : env -> evar_map -> unsafe_judgment -> std_ppcmds * std_ppcmds
-val pr_ljudge : unsafe_judgment -> std_ppcmds * std_ppcmds
+val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> std_ppcmds * std_ppcmds
+val pr_ljudge : EConstr.unsafe_judgment -> std_ppcmds * std_ppcmds
val pr_lglob_constr_env : env -> glob_constr -> std_ppcmds
val pr_lglob_constr : glob_constr -> std_ppcmds
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 2f8af6b44..84ca0aa8f 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -185,8 +185,7 @@ let set_typeclasses_depth =
optwrite = set_typeclasses_depth; }
let pr_ev evs ev =
- Printer.pr_constr_env (Goal.V82.env evs ev) evs
- (Evarutil.nf_evar evs (EConstr.Unsafe.to_constr (Goal.V82.concl evs ev)))
+ Printer.pr_econstr_env (Goal.V82.env evs ev) evs (Goal.V82.concl evs ev)
(** Typeclasses instance search tactic / eauto *)
@@ -764,7 +763,7 @@ module V85 = struct
if foundone == None && !typeclasses_debug > 0 then
Feedback.msg_debug
(pr_depth info.auto_depth ++ str": no match for " ++
- Printer.pr_constr_env (Goal.V82.env s gl) s (EConstr.Unsafe.to_constr concl) ++
+ Printer.pr_econstr_env (Goal.V82.env s gl) s concl ++
spc () ++ str ", " ++ int (List.length poss) ++
str" possibilities");
match foundone with
@@ -1005,7 +1004,7 @@ module Search = struct
if !typeclasses_debug > 0 then
Feedback.msg_debug
(pr_depth info.search_depth ++ str": looking for " ++
- Printer.pr_constr_env (Goal.env gl) s (EConstr.Unsafe.to_constr concl) ++
+ Printer.pr_econstr_env (Goal.env gl) s concl ++
(if backtrack then str" with backtracking"
else str" without backtracking"));
let secvars = compute_secvars gl in
@@ -1120,7 +1119,7 @@ module Search = struct
if !foundone == false && !typeclasses_debug > 0 then
Feedback.msg_debug
(pr_depth info.search_depth ++ str": no match for " ++
- Printer.pr_constr_env (Goal.env gl) s (EConstr.Unsafe.to_constr concl) ++
+ Printer.pr_econstr_env (Goal.env gl) s concl ++
spc () ++ str ", " ++ int (List.length poss) ++
str" possibilities");
match e with
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 9e9635e8a..2446b6996 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -792,7 +792,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
else begin
if not eapply then failwith "make_apply_entry";
if verbose then
- Feedback.msg_info (str "the hint: eapply " ++ pr_lconstr (EConstr.Unsafe.to_constr c) ++
+ Feedback.msg_info (str "the hint: eapply " ++ pr_leconstr_env env sigma' c ++
str " will only be used by eauto");
(Some hd,
{ pri = (match pri with None -> nb_hyp sigma' cty + nmiss | Some p -> p);
@@ -813,7 +813,7 @@ let pr_hint_term env sigma ctx = function
| IsGlobRef gr -> pr_global gr
| IsConstr (c, ctx) ->
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
- pr_constr_env env sigma (EConstr.Unsafe.to_constr c)
+ pr_econstr_env env sigma c
(** We need an object to record the side-effect of registering
global universes associated with a hint. *)
@@ -863,7 +863,7 @@ let make_resolves env sigma flags pri poly ?name cr =
in
if List.is_empty ents then
user_err ~hdr:"Hint"
- (pr_lconstr (EConstr.Unsafe.to_constr c) ++ spc() ++
+ (pr_leconstr_env env sigma c ++ spc() ++
(if pi1 flags then str"cannot be used as a hint."
else str "can be used as a hint only for eauto."));
ents
@@ -1360,7 +1360,7 @@ let make_db_list dbnames =
(* Functions for printing the hints *)
(**************************************************************************)
-let pr_hint_elt (c, _, _) = pr_constr (EConstr.Unsafe.to_constr c)
+let pr_hint_elt (c, _, _) = pr_econstr c
let pr_hint h = match h.obj with
| Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt c)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index ef3bfc9d0..2d59285e6 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -42,7 +42,7 @@ let nlocal_def (na, b, t) =
let no_inductive_inconstr env sigma constr =
(str "Cannot recognize an inductive predicate in " ++
- pr_lconstr_env env sigma (EConstr.Unsafe.to_constr constr) ++
+ pr_leconstr_env env sigma constr ++
str "." ++ spc () ++ str "If there is one, may be the structure of the arity" ++
spc () ++ str "or of the type of constructors" ++ spc () ++
str "is hidden by constant definitions.")
@@ -277,14 +277,12 @@ let lemInv id c gls =
Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls
with
| NoSuchBinding ->
- let c = EConstr.Unsafe.to_constr c in
user_err
- (hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma."))
+ (hov 0 (pr_econstr_env (Refiner.pf_env gls) (Refiner.project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
| UserError (a,b) ->
- let c = EConstr.Unsafe.to_constr c in
user_err ~hdr:"LemInv"
(str "Cannot refine current goal with the lemma " ++
- pr_lconstr_env (Refiner.pf_env gls) (Refiner.project gls) c)
+ pr_leconstr_env (Refiner.pf_env gls) (Refiner.project gls) c)
let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4e833eb55..dcaa15fd8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3073,7 +3073,7 @@ let warn_unused_intro_pattern =
strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern")
++ str": " ++ prlist_with_sep spc
(Miscprint.pr_intro_pattern
- (fun c -> Printer.pr_constr (EConstr.Unsafe.to_constr (fst (run_delayed (Global.env()) Evd.empty c))))) names)
+ (fun c -> Printer.pr_econstr (fst (run_delayed (Global.env()) Evd.empty c)))) names)
let check_unused_names names =
if not (List.is_empty names) && Flags.is_verbose () then
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 7eb189ef5..3c2fe46b3 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -86,11 +86,11 @@ let rec contract3' env a b c = function
let to_unsafe_judgment j = on_judgment EConstr.Unsafe.to_constr j
let j_nf_betaiotaevar sigma j =
- { uj_val = Evarutil.nf_evar sigma j.uj_val;
- uj_type = EConstr.Unsafe.to_constr (Reductionops.nf_betaiota sigma (EConstr.of_constr j.uj_type)) }
+ { uj_val = Evarutil.nf_evar sigma (EConstr.Unsafe.to_constr j.uj_val);
+ uj_type = EConstr.Unsafe.to_constr (Reductionops.nf_betaiota sigma j.uj_type) }
let jv_nf_betaiotaevar sigma jl =
- Array.map (j_nf_betaiotaevar sigma) jl
+ Array.map (fun j -> on_judgment EConstr.of_constr (j_nf_betaiotaevar sigma j)) jl
(** Printers *)
@@ -172,7 +172,6 @@ let explain_unbound_var env v =
let explain_not_type env sigma j =
let j = Evarutil.j_nf_evar sigma j in
- let j = to_unsafe_judgment j in
let pe = pr_ne_context_of (str "In environment") env sigma in
let pc,pt = pr_ljudge_env env sigma j in
pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++
@@ -180,17 +179,15 @@ let explain_not_type env sigma j =
str "which should be Set, Prop or Type."
let explain_bad_assumption env sigma j =
- let j = to_unsafe_judgment j in
let pe = pr_ne_context_of (str "In environment") env sigma in
let pc,pt = pr_ljudge_env env sigma j in
pe ++ str "Cannot declare a variable or hypothesis over the term" ++
brk(1,1) ++ pc ++ spc () ++ str "of type" ++ spc () ++ pt ++ spc () ++
str "because this term is not a type."
-let explain_reference_variables id c =
- let c = EConstr.Unsafe.to_constr c in
+let explain_reference_variables sigma id c =
(* c is intended to be a global reference *)
- let pc = pr_global (Globnames.global_of_constr c) in
+ let pc = pr_global (fst (Termops.global_of_constr sigma c)) in
pc ++ strbrk " depends on the variable " ++ pr_id id ++
strbrk " which is not declared in the context."
@@ -207,11 +204,10 @@ let pr_puniverses f env (c,u) =
else mt())
let explain_elim_arity env sigma ind sorts c pj okinds =
- let c = EConstr.Unsafe.to_constr c in
let pj = to_unsafe_judgment pj in
let env = make_all_name_different env in
let pi = pr_inductive env (fst ind) in
- let pc = pr_lconstr_env env sigma c in
+ let pc = pr_leconstr_env env sigma c in
let msg = match okinds with
| Some(kp,ki,explanation) ->
let pki = pr_sort_family ki in
@@ -267,13 +263,11 @@ let explain_number_branches env sigma cj expn =
str "expects " ++ int expn ++ str " branches."
let explain_ill_formed_branch env sigma c ci actty expty =
- let c = EConstr.Unsafe.to_constr c in
let actty = EConstr.Unsafe.to_constr actty in
let expty = EConstr.Unsafe.to_constr expty in
let simp t = Reduction.nf_betaiota env (Evarutil.nf_evar sigma t) in
- let c = Evarutil.nf_evar sigma c in
let env = make_all_name_different env in
- let pc = pr_lconstr_env env sigma c in
+ let pc = pr_leconstr_env env sigma c in
let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in
strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++
spc () ++ strbrk "the branch for constructor" ++ spc () ++
@@ -282,11 +276,9 @@ let explain_ill_formed_branch env sigma c ci actty expty =
str "which should be" ++ brk(1,1) ++ pe ++ str "."
let explain_generalization env sigma (name,var) j =
- let var = EConstr.Unsafe.to_constr var in
- let j = to_unsafe_judgment j in
let pe = pr_ne_context_of (str "In environment") env sigma in
- let pv = pr_ltype_env env sigma var in
- let (pc,pt) = pr_ljudge_env (push_rel_assum (name,EConstr.of_constr var) env) sigma j in
+ let pv = pr_letype_env env sigma var in
+ let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) env) sigma j in
pe ++ str "Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++
str "over" ++ brk(1,1) ++ pc ++ str "," ++ spc () ++
str "it has type" ++ spc () ++ pt ++
@@ -297,19 +289,16 @@ let explain_unification_error env sigma p1 p2 = function
| Some e ->
let rec aux p1 p2 = function
| OccurCheck (evk,rhs) ->
- let rhs = EConstr.to_constr sigma rhs in
[str "cannot define " ++ quote (pr_existential_key sigma evk) ++
- strbrk " with term " ++ pr_lconstr_env env sigma rhs ++
+ strbrk " with term " ++ pr_leconstr_env env sigma rhs ++
strbrk " that would depend on itself"]
| NotClean ((evk,args),env,c) ->
- let c = EConstr.to_constr sigma c in
- let args = Array.map (EConstr.to_constr sigma) args in
[str "cannot instantiate " ++ quote (pr_existential_key sigma evk)
- ++ strbrk " because " ++ pr_lconstr_env env sigma c ++
+ ++ strbrk " because " ++ pr_leconstr_env env sigma c ++
strbrk " is not in its scope" ++
(if Array.is_empty args then mt() else
strbrk ": available arguments are " ++
- pr_sequence (pr_lconstr_env env sigma) (List.rev (Array.to_list args)))]
+ pr_sequence (pr_leconstr_env env sigma) (List.rev (Array.to_list args)))]
| NotSameArgSize | NotSameHead | NoCanonicalStructure ->
(* Error speaks from itself *) []
| ConversionFailed (env,t1,t2) ->
@@ -357,11 +346,9 @@ let explain_unification_error env sigma p1 p2 = function
prlist_with_sep pr_semicolon (fun x -> x) l ++ str ")"
let explain_actual_type env sigma j t reason =
- let j = to_unsafe_judgment j in
- let t = EConstr.Unsafe.to_constr t in
let env = make_all_name_different env in
let j = j_nf_betaiotaevar sigma j in
- let t = Reductionops.nf_betaiota sigma (EConstr.of_constr t) in
+ let t = Reductionops.nf_betaiota sigma t in
let t = EConstr.Unsafe.to_constr t in
(** Actually print *)
let pe = pr_ne_context_of (str "In environment") env sigma in
@@ -377,14 +364,11 @@ let explain_actual_type env sigma j t reason =
let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
let exptyp = EConstr.Unsafe.to_constr exptyp in
- let actualtyp = EConstr.Unsafe.to_constr actualtyp in
- let randl = Array.map to_unsafe_judgment randl in
let randl = jv_nf_betaiotaevar sigma randl in
let exptyp = Evarutil.nf_evar sigma exptyp in
- let actualtyp = Reductionops.nf_betaiota sigma (EConstr.of_constr actualtyp) in
+ let actualtyp = Reductionops.nf_betaiota sigma actualtyp in
let actualtyp = EConstr.Unsafe.to_constr actualtyp in
let rator = Evarutil.j_nf_evar sigma rator in
- let rator = to_unsafe_judgment rator in
let env = make_all_name_different env in
let actualtyp, exptyp = pr_explicit env sigma actualtyp exptyp in
let nargs = Array.length randl in
@@ -448,7 +432,7 @@ let explain_not_product env sigma c =
(* TODO: use the names *)
(* (co)fixpoints *)
let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
- let pr_lconstr_env env sigma c = pr_lconstr_env env sigma (EConstr.Unsafe.to_constr c) in
+ let pr_lconstr_env env sigma c = pr_leconstr_env env sigma c in
let prt_name i =
match names.(i) with
Name id -> str "Recursive definition of " ++ pr_id id
@@ -549,17 +533,14 @@ let explain_ill_typed_rec_body env sigma i names vdefj vargs =
str "while it should be" ++ spc () ++ pv ++ str "."
let explain_cant_find_case_type env sigma c =
- let c = EConstr.Unsafe.to_constr c in
- let c = Evarutil.nf_evar sigma c in
let env = make_all_name_different env in
- let pe = pr_lconstr_env env sigma c in
+ let pe = pr_leconstr_env env sigma c in
str "Cannot infer the return type of pattern-matching on" ++ ws 1 ++
pe ++ str "."
let explain_occur_check env sigma ev rhs =
- let rhs = EConstr.to_constr sigma rhs in
let env = make_all_name_different env in
- let pt = pr_lconstr_env env sigma rhs in
+ let pt = pr_leconstr_env env sigma rhs in
str "Cannot define " ++ pr_existential_key sigma ev ++ str " with term" ++
brk(1,1) ++ pt ++ spc () ++ str "that would depend on itself."
@@ -665,12 +646,9 @@ let explain_cannot_unify env sigma m n e =
str "with" ++ brk(1,1) ++ pn ++ ppreason ++ str "."
let explain_cannot_unify_local env sigma m n subn =
- let m = EConstr.to_constr sigma m in
- let n = EConstr.to_constr sigma n in
- let subn = EConstr.to_constr sigma subn in
- let pm = pr_lconstr_env env sigma m in
- let pn = pr_lconstr_env env sigma n in
- let psubn = pr_lconstr_env env sigma subn in
+ let pm = pr_leconstr_env env sigma m in
+ let pn = pr_leconstr_env env sigma n in
+ let psubn = pr_leconstr_env env sigma subn in
str "Unable to unify" ++ brk(1,1) ++ pm ++ spc () ++
str "with" ++ brk(1,1) ++ pn ++ spc () ++ str "as" ++ brk(1,1) ++
psubn ++ str " contains local variables."
@@ -740,7 +718,7 @@ let explain_type_error env sigma err =
| BadAssumption c ->
explain_bad_assumption env sigma c
| ReferenceVariables (id,c) ->
- explain_reference_variables id c
+ explain_reference_variables sigma id c
| ElimArity (ind, aritylst, c, pj, okinds) ->
explain_elim_arity env sigma ind aritylst c pj okinds
| CaseNotInductive cj ->
@@ -1117,8 +1095,7 @@ let explain_non_linear_proof c =
spc () ++ str "because a metavariable has several occurrences."
let explain_meta_in_type c =
- let c = EConstr.Unsafe.to_constr c in
- str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_lconstr c ++
+ str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_leconstr c ++
str " of another meta"
let explain_no_such_hyp id =
@@ -1170,7 +1147,7 @@ let error_ill_formed_constructor env id c v nparams nargs =
let pr_ltype_using_barendregt_convention_env env c =
(* Use goal_concl_style as an approximation of Barendregt's convention (?) *)
- quote (pr_goal_concl_style_env env Evd.empty c)
+ quote (pr_goal_concl_style_env env Evd.empty (EConstr.of_constr c))
let error_bad_ind_parameters env c n v1 v2 =
let pc = pr_ltype_using_barendregt_convention_env env c in
@@ -1364,7 +1341,6 @@ let map_ptype_error f = function
let explain_reduction_tactic_error = function
| Tacred.InvalidAbstraction (env,sigma,c,(env',e)) ->
let e = map_ptype_error EConstr.of_constr e in
- let c = EConstr.to_constr sigma c in
str "The abstracted term" ++ spc () ++
quote (pr_goal_concl_style_env env sigma c) ++
spc () ++ str "is not well typed." ++ fnl () ++
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 25b639fb0..ee2aacfc5 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1580,15 +1580,16 @@ let vernac_check_may_eval redexp glopt rc =
let c = nf c in
let j =
if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then
- let j = Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' (EConstr.of_constr c)) in
- Termops.on_judgment EConstr.Unsafe.to_constr j
+ Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' (EConstr.of_constr c))
else
(* OK to call kernel which does not support evars *)
- Arguments_renaming.rename_typing env c in
+ Termops.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c)
+ in
match redexp with
| None ->
- let l = Evar.Set.union (Evd.evars_of_term j.Environ.uj_val) (Evd.evars_of_term j.Environ.uj_type) in
- let j = { j with Environ.uj_type = EConstr.Unsafe.to_constr (Reductionops.nf_betaiota sigma' (EConstr.of_constr j.Environ.uj_type)) } in
+ let evars_of_term c = Evarutil.undefined_evars_of_term sigma' c in
+ let l = Evar.Set.union (evars_of_term j.Environ.uj_val) (evars_of_term j.Environ.uj_type) in
+ let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in
Feedback.msg_notice (print_judgment env sigma' j ++
pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
Printer.pr_universe_ctx sigma uctx)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 04:02:04 +0000