aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml79
-rw-r--r--engine/eConstr.mli15
-rw-r--r--engine/evarutil.ml6
-rw-r--r--engine/evarutil.mli14
-rw-r--r--engine/evd.ml15
-rw-r--r--engine/evd.mli4
-rw-r--r--engine/namegen.ml3
-rw-r--r--engine/proofview.ml10
-rw-r--r--engine/termops.ml39
-rw-r--r--engine/termops.mli4
-rw-r--r--engine/uState.ml10
11 files changed, 101 insertions, 98 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 54d3ce6cf7..5a05150d44 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -295,7 +295,7 @@ let decompose_lam_assum sigma c =
let decompose_lam_n_assum sigma n c =
let open Rel.Declaration in
if n < 0 then
- error "decompose_lam_n_assum: integer parameter must be positive";
+ user_err Pp.(str "decompose_lam_n_assum: integer parameter must be positive");
let rec lamdec_rec l n c =
if Int.equal n 0 then l,c
else
@@ -303,14 +303,14 @@ let decompose_lam_n_assum sigma n c =
| Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
| LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c
| Cast (c,_,_) -> lamdec_rec l n c
- | c -> error "decompose_lam_n_assum: not enough abstractions"
+ | c -> user_err Pp.(str "decompose_lam_n_assum: not enough abstractions")
in
lamdec_rec Context.Rel.empty n c
let decompose_lam_n_decls sigma n =
let open Rel.Declaration in
if n < 0 then
- error "decompose_lam_n_decls: integer parameter must be positive";
+ user_err Pp.(str "decompose_lam_n_decls: integer parameter must be positive");
let rec lamdec_rec l n c =
if Int.equal n 0 then l,c
else
@@ -318,7 +318,7 @@ let decompose_lam_n_decls sigma n =
| Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
| LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c
| Cast (c,_,_) -> lamdec_rec l n c
- | c -> error "decompose_lam_n_decls: not enough abstractions"
+ | c -> user_err Pp.(str "decompose_lam_n_decls: not enough abstractions")
in
lamdec_rec Context.Rel.empty n
@@ -363,7 +363,7 @@ let decompose_prod_assum sigma c =
let decompose_prod_n_assum sigma n c =
let open Rel.Declaration in
if n < 0 then
- error "decompose_prod_n_assum: integer parameter must be positive";
+ user_err Pp.(str "decompose_prod_n_assum: integer parameter must be positive");
let rec prodec_rec l n c =
if Int.equal n 0 then l,c
else
@@ -371,7 +371,7 @@ let decompose_prod_n_assum sigma n c =
| Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
| LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c
| Cast (c,_,_) -> prodec_rec l n c
- | c -> error "decompose_prod_n_assum: not enough assumptions"
+ | c -> user_err Pp.(str "decompose_prod_n_assum: not enough assumptions")
in
prodec_rec Context.Rel.empty n c
@@ -638,22 +638,54 @@ let eq_constr_universes_proj env sigma m n =
let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in
if res then Some !cstrs else None
+open Context
+open Environ
+
+let cast_list : type a b. (a,b) eq -> a list -> b list =
+ fun Refl x -> x
+
+let cast_list_snd : type a b. (a,b) eq -> ('c * a) list -> ('c * b) list =
+ fun Refl x -> x
+
+let cast_rel_decl :
+ type a b. (a,b) eq -> (a, a) Rel.Declaration.pt -> (b, b) Rel.Declaration.pt =
+ fun Refl x -> x
+
+let cast_rel_context :
+ type a b. (a,b) eq -> (a, a) Rel.pt -> (b, b) Rel.pt =
+ fun Refl x -> x
+
+let cast_named_decl :
+ type a b. (a,b) eq -> (a, a) Named.Declaration.pt -> (b, b) Named.Declaration.pt =
+ fun Refl x -> x
+
+let cast_named_context :
+ type a b. (a,b) eq -> (a, a) Named.pt -> (b, b) Named.pt =
+ fun Refl x -> x
+
+
module Vars =
struct
exception LocalOccur
let to_constr = unsafe_to_constr
+let to_rel_decl = unsafe_to_rel_decl
+
+type substl = t list
(** Operations that commute with evar-normalization *)
let lift n c = of_constr (Vars.lift n (to_constr c))
let liftn n m c = of_constr (Vars.liftn n m (to_constr c))
-let substnl subst n c = of_constr (Vars.substnl (List.map to_constr subst) n (to_constr c))
-let substl subst c = of_constr (Vars.substl (List.map to_constr subst) (to_constr c))
+let substnl subst n c = of_constr (Vars.substnl (cast_list unsafe_eq subst) n (to_constr c))
+let substl subst c = of_constr (Vars.substl (cast_list unsafe_eq subst) (to_constr c))
let subst1 c r = of_constr (Vars.subst1 (to_constr c) (to_constr r))
+let substnl_decl subst n d = of_rel_decl (Vars.substnl_decl (cast_list unsafe_eq subst) n (to_rel_decl d))
+let substl_decl subst d = of_rel_decl (Vars.substl_decl (cast_list unsafe_eq subst) (to_rel_decl d))
+let subst1_decl c d = of_rel_decl (Vars.subst1_decl (to_constr c) (to_rel_decl d))
+
let replace_vars subst c =
- let map (id, c) = (id, to_constr c) in
- of_constr (Vars.replace_vars (List.map map subst) (to_constr c))
+ of_constr (Vars.replace_vars (cast_list_snd unsafe_eq subst) (to_constr c))
let substn_vars n subst c = of_constr (Vars.substn_vars n subst (to_constr c))
let subst_vars subst c = of_constr (Vars.subst_vars subst (to_constr c))
let subst_var subst c = of_constr (Vars.subst_var subst (to_constr c))
@@ -685,7 +717,8 @@ let closedn sigma n c =
let closed0 sigma c = closedn sigma 0 c
let subst_of_rel_context_instance ctx subst =
- List.map of_constr (Vars.subst_of_rel_context_instance (List.map unsafe_to_rel_decl ctx) (List.map to_constr subst))
+ cast_list (sym unsafe_eq)
+ (Vars.subst_of_rel_context_instance (cast_rel_context unsafe_eq ctx) (cast_list unsafe_eq subst))
end
@@ -728,27 +761,6 @@ let mkNamedLambda_or_LetIn decl c =
let it_mkProd_or_LetIn t ctx = List.fold_left (fun c d -> mkProd_or_LetIn d c) t ctx
let it_mkLambda_or_LetIn t ctx = List.fold_left (fun c d -> mkLambda_or_LetIn d c) t ctx
-open Context
-open Environ
-
-let sym : type a b. (a, b) eq -> (b, a) eq = fun Refl -> Refl
-
-let cast_rel_decl :
- type a b. (a,b) eq -> (a, a) Rel.Declaration.pt -> (b, b) Rel.Declaration.pt =
- fun Refl x -> x
-
-let cast_rel_context :
- type a b. (a,b) eq -> (a, a) Rel.pt -> (b, b) Rel.pt =
- fun Refl x -> x
-
-let cast_named_decl :
- type a b. (a,b) eq -> (a, a) Named.Declaration.pt -> (b, b) Named.Declaration.pt =
- fun Refl x -> x
-
-let cast_named_context :
- type a b. (a,b) eq -> (a, a) Named.pt -> (b, b) Named.pt =
- fun Refl x -> x
-
let push_rel d e = push_rel (cast_rel_decl unsafe_eq d) e
let push_rel_context d e = push_rel_context (cast_rel_context unsafe_eq d) e
let push_named d e = push_named (cast_named_decl unsafe_eq d) e
@@ -770,6 +782,9 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
Sigma.fresh_global ?loc ?rigid ?names env sigma reference in
Sigma.Sigma (of_constr t,sigma,p)
+let is_global sigma gr c =
+ Globnames.is_global gr (to_constr sigma c)
+
module Unsafe =
struct
let to_sorts = ESorts.unsafe_to_sorts
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 693b592fd4..9f45187cff 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -205,12 +205,21 @@ val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
module Vars :
sig
+
+(** See vars.mli for the documentation of the functions below *)
+
+type substl = t list
+
val lift : int -> t -> t
val liftn : int -> int -> t -> t
-val substnl : t list -> int -> t -> t
-val substl : t list -> t -> t
+val substnl : substl -> int -> t -> t
+val substl : substl -> t -> t
val subst1 : t -> t -> t
+val substnl_decl : substl -> int -> rel_declaration -> rel_declaration
+val substl_decl : substl -> rel_declaration -> rel_declaration
+val subst1_decl : t -> rel_declaration -> rel_declaration
+
val replace_vars : (Id.t * t) list -> t -> t
val substn_vars : int -> Id.t list -> t -> t
val subst_vars : Id.t list -> t -> t
@@ -252,6 +261,8 @@ val fresh_global :
?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
'r Sigma.t -> Globnames.global_reference -> (t, 'r) Sigma.sigma
+val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool
+
(** {5 Extra} *)
val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index e85c1f6fd8..3ef725cbbd 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -365,12 +365,12 @@ let push_rel_context_to_named_context env sigma typ =
* Entry points to define new evars *
*------------------------------------*)
-let default_source = (Loc.ghost,Evar_kinds.InternalHole)
+let default_source = Loc.tag @@ Evar_kinds.InternalHole
-let restrict_evar evd evk filter candidates =
+let restrict_evar evd evk filter ?src candidates =
let evd = Sigma.to_evar_map evd in
let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
- let evd, evk' = Evd.restrict evk filter ?candidates evd in
+ let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd)
let new_pure_evar_full evd evi =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index ca9591e71b..496ec5bc43 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -22,13 +22,13 @@ val mk_new_meta : unit -> constr
(** {6 Creating a fresh evar given their type and context} *)
val new_evar :
- env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+ env -> 'r Sigma.t -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t ->
?naming:Misctypes.intro_pattern_naming_expr ->
?principal:bool -> types -> (constr, 'r) Sigma.sigma
val new_pure_evar :
- named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+ named_context_val -> 'r Sigma.t -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t ->
?naming:Misctypes.intro_pattern_naming_expr ->
?principal:bool -> types -> (evar, 'r) Sigma.sigma
@@ -37,7 +37,7 @@ val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma
(** the same with side-effects *)
val e_new_evar :
- env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+ env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t ->
?naming:Misctypes.intro_pattern_naming_expr ->
?principal:bool -> types -> constr
@@ -45,19 +45,19 @@ val e_new_evar :
(** Create a new Type existential variable, as we keep track of
them during type-checking and unification. *)
val new_type_evar :
- env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+ env -> 'r Sigma.t -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
(constr * sorts, 'r) Sigma.sigma
val e_new_type_evar : env -> evar_map ref ->
- ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+ ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t ->
- constr list option -> (existential_key, 'r) Sigma.sigma
+ ?src:Evar_kinds.t Loc.located -> constr list option -> (existential_key, 'r) Sigma.sigma
(** Polymorphic constants *)
@@ -72,7 +72,7 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr
as a telescope) is [sign] *)
val new_evar_instance :
named_context_val -> 'r Sigma.t -> types ->
- ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list ->
+ ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list ->
?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
?principal:bool ->
constr list -> (constr, 'r) Sigma.sigma
diff --git a/engine/evd.ml b/engine/evd.ml
index db048bbd6e..48fceae9ec 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -149,7 +149,7 @@ let make_evar hyps ccl = {
evar_hyps = hyps;
evar_body = Evar_empty;
evar_filter = Filter.identity;
- evar_source = (Loc.ghost,Evar_kinds.InternalHole);
+ evar_source = Loc.tag @@ Evar_kinds.InternalHole;
evar_candidates = None;
evar_extra = Store.empty
}
@@ -653,12 +653,13 @@ let define evk body evd =
let evar_names = EvNames.remove_name_defined evk evd.evar_names in
{ evd with defn_evars; undf_evars; last_mods; evar_names }
-let restrict evk filter ?candidates evd =
+let restrict evk filter ?candidates ?src evd =
let evk' = new_untyped_evar () in
let evar_info = EvMap.find evk evd.undf_evars in
let evar_info' =
{ evar_info with evar_filter = filter;
evar_candidates = candidates;
+ evar_source = (match src with None -> evar_info.evar_source | Some src -> src);
evar_extra = Store.empty } in
let last_mods = match evd.conv_pbs with
| [] -> evd.last_mods
@@ -704,7 +705,7 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) =
| _ ->
match kind_of_term (fst (decompose_app t2)) with
| Evar (evk2,_) -> fst (evar_source evk2 evd)
- | _ -> Loc.ghost
+ | _ -> None
(** The following functions return the set of evars immediately
contained in the object *)
@@ -790,7 +791,7 @@ let make_evar_universe_context e l =
| Some us ->
List.fold_left
(fun uctx (loc,id) ->
- fst (UState.new_univ_variable ~loc univ_rigid (Some (Id.to_string id)) uctx))
+ fst (UState.new_univ_variable ?loc univ_rigid (Some (Id.to_string id)) uctx))
uctx us
(****************************************)
@@ -952,7 +953,7 @@ let declare_principal_goal evk evd =
| None -> { evd with
future_goals = evk::evd.future_goals;
principal_future_goal=Some evk; }
- | Some _ -> CErrors.error "Only one main subgoal per instantiation."
+ | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.")
let future_goals evd = evd.future_goals
@@ -1082,8 +1083,8 @@ let retract_coercible_metas evd =
let evar_source_of_meta mv evd =
match meta_name evd mv with
- | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar)
- | Name id -> (Loc.ghost,Evar_kinds.VarInstance id)
+ | Anonymous -> Loc.tag Evar_kinds.GoalEvar
+ | Name id -> Loc.tag @@ Evar_kinds.VarInstance id
let dependent_evar_ident ev evd =
let evi = find evd ev in
diff --git a/engine/evd.mli b/engine/evd.mli
index 9c40c8b715..86755c360b 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -240,7 +240,7 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool ->
(** {6 Misc} *)
val restrict : evar -> Filter.t -> ?candidates:constr list ->
- evar_map -> evar_map * evar
+ ?src:Evar_kinds.t located -> evar_map -> evar_map * evar
(** Restrict an undefined evar into a new evar by filtering context and
possibly limiting the instances to a set of candidates *)
@@ -414,7 +414,7 @@ val extract_changed_conv_pbs : evar_map ->
(Evar.Set.t -> evar_constraint -> bool) ->
evar_map * evar_constraint list
val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
-val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t
+val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option
(** The following functions return the set of evars immediately
contained in the object; need the term to be evar-normal otherwise
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 3b979f206e..5bd62273c8 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -418,8 +418,7 @@ let use_h_based_elimination_names () =
open Goptions
let _ = declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "use of \"H\"-based proposition names in elimination tactics";
optkey = ["Standard";"Proposition";"Elimination";"Names"];
optread = (fun () -> !h_based_elimination_names);
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 99bd4bc4ff..29bb1ef397 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -66,7 +66,7 @@ let dependent_init =
for type classes. *)
let store = Evd.Store.set Evd.Store.empty typeclass_resolvable () in
(* Goals don't have a source location. *)
- let src = (Loc.ghost,Evar_kinds.GoalEvar) in
+ let src = Loc.tag @@ Evar_kinds.GoalEvar in
(* Main routine *)
let rec aux = function
| TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
@@ -289,7 +289,7 @@ let tclONCE = Proof.once
exception MoreThanOneSuccess
let _ = CErrors.register_handler begin function
- | MoreThanOneSuccess -> CErrors.error "This tactic has more than one success."
+ | MoreThanOneSuccess -> CErrors.user_err Pp.(str "This tactic has more than one success.")
| _ -> raise CErrors.Unhandled
end
@@ -696,6 +696,12 @@ let mark_in_evm ~goal evd content =
let info =
if goal then
{ info with Evd.evar_source = match info.Evd.evar_source with
+ (* Two kinds for goal evars:
+ - GoalEvar (morally not dependent)
+ - VarInstance (morally dependent of some name).
+ This is a heuristic for naming these evars. *)
+ | loc, (Evar_kinds.QuestionMark (_,Names.Name id) |
+ Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
| _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
| loc,_ -> loc,Evar_kinds.GoalEvar }
else info
diff --git a/engine/termops.ml b/engine/termops.ml
index 19e62f8e62..cbb0f0779f 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -31,10 +31,6 @@ let pr_sort_family = function
| InProp -> (str "Prop")
| InType -> (str "Type")
-let pr_name = function
- | Name id -> pr_id id
- | Anonymous -> str "_"
-
let pr_con sp = str(string_of_con sp)
let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
@@ -42,7 +38,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
hov 1
(str"fix " ++ int i ++ spc() ++ str"{" ++
v 0 (prlist_with_sep spc (fun (na,i,ty,bd) ->
- pr_name na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++
+ Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++
cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
str"}")
@@ -65,10 +61,10 @@ let rec pr_constr c = match kind_of_term c with
(str"(" ++ pr_constr t ++ str " ->" ++ spc() ++
pr_constr c ++ str")")
| Lambda (na,t,c) -> hov 1
- (str"fun " ++ pr_name na ++ str":" ++
+ (str"fun " ++ Name.print na ++ str":" ++
pr_constr t ++ str" =>" ++ spc() ++ pr_constr c)
| LetIn (na,b,t,c) -> hov 0
- (str"let " ++ pr_name na ++ str":=" ++ pr_constr b ++
+ (str"let " ++ Name.print na ++ str":=" ++ pr_constr b ++
str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++
pr_constr c)
| App (c,l) -> hov 1
@@ -93,7 +89,7 @@ let rec pr_constr c = match kind_of_term c with
hov 1
(str"cofix " ++ int i ++ spc() ++ str"{" ++
v 0 (prlist_with_sep spc (fun (na,ty,bd) ->
- pr_name na ++ str":" ++ pr_constr ty ++
+ Name.print na ++ str":" ++ pr_constr ty ++
cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
str"}")
@@ -112,6 +108,7 @@ let pr_evar_suggested_name evk sigma =
| None -> match evi.evar_source with
| _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
| _,Evar_kinds.VarInstance id -> id
+ | _,Evar_kinds.QuestionMark (_,Name id) -> id
| _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
| _ ->
let env = reset_with_named_context evi.evar_hyps (Global.env()) in
@@ -308,8 +305,8 @@ let pr_evar_universe_context ctx =
let print_env_short env =
let print_constr = print_kconstr in
let pr_rel_decl = function
- | RelDecl.LocalAssum (n,_) -> pr_name n
- | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")"
+ | RelDecl.LocalAssum (n,_) -> Name.print n
+ | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := " ++ print_constr b ++ str ")"
in
let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in
let nc = List.rev (named_context env) in
@@ -1468,25 +1465,3 @@ let env_rel_context_chop k env =
let ctx1,ctx2 = List.chop k rels in
push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
ctx1
-
-(*******************************************)
-(* Functions to deal with impossible cases *)
-(*******************************************)
-let impossible_default_case = ref None
-
-let set_impossible_default_clause c = impossible_default_case := Some c
-
-let coq_unit_judge =
- let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in
- let na1 = Name (Id.of_string "A") in
- let na2 = Name (Id.of_string "H") in
- fun () ->
- match !impossible_default_case with
- | Some fn ->
- let (id,type_of_id), ctx = fn () in
- make_judge id type_of_id, ctx
- | None ->
- (* In case the constants id/ID are not defined *)
- make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1)))
- (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))),
- Univ.ContextSet.empty
diff --git a/engine/termops.mli b/engine/termops.mli
index fe6dfb0ce1..58837ba033 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -275,10 +275,6 @@ val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) puns
val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
-(** {6 Functions to deal with impossible cases } *)
-val set_impossible_default_clause : (unit -> (Constr.constr * Constr.types) Univ.in_universe_context_set) -> unit
-val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set
-
(** {5 Debug pretty-printers} *)
open Evd
diff --git a/engine/uState.ml b/engine/uState.ml
index e27d0536d6..acef901432 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -188,7 +188,7 @@ let process_universe_constraints ctx cstrs =
| _ -> local
else
begin match Univ.Universe.level r with
- | None -> error ("Algebraic universe on the right")
+ | None -> user_err Pp.(str "Algebraic universe on the right")
| Some r' ->
if Univ.Level.is_small r' then
let levels = Univ.Universe.levels l in
@@ -258,7 +258,7 @@ let universe_context ?names ctx =
let l =
try UNameMap.find (Id.to_string id) (fst ctx.uctx_names)
with Not_found ->
- user_err ~loc ~hdr:"universe_context"
+ user_err ?loc ~hdr:"universe_context"
(str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.")
in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc))
pl ([], [], levels)
@@ -269,10 +269,10 @@ let universe_context ?names ctx =
try
let info =
Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in
- Option.default Loc.ghost info.uloc
- with Not_found -> Loc.ghost
+ info.uloc
+ with Not_found -> None
in
- user_err ~loc ~hdr:"universe_context"
+ user_err ?loc ~hdr:"universe_context"
((str(CString.plural n "Universe") ++ spc () ++
Univ.LSet.pr (pr_uctx_level ctx) left ++
spc () ++ str (CString.conjugate_verb_to_be n) ++
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 08:56:54 +0000