aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml46
-rw-r--r--pretyping/coercion.ml12
-rw-r--r--pretyping/detyping.ml5
-rw-r--r--pretyping/evarconv.ml8
-rw-r--r--pretyping/evarsolve.ml4
-rw-r--r--pretyping/glob_ops.ml198
-rw-r--r--pretyping/glob_ops.mli3
-rw-r--r--pretyping/indrec.ml6
-rw-r--r--pretyping/inductiveops.ml2
-rw-r--r--pretyping/locusops.ml2
-rw-r--r--pretyping/nativenorm.ml4
-rw-r--r--pretyping/patternops.ml23
-rw-r--r--pretyping/pretyping.ml24
-rw-r--r--pretyping/program.ml20
-rw-r--r--pretyping/program.mli4
-rw-r--r--pretyping/reductionops.ml22
-rw-r--r--pretyping/retyping.ml2
-rw-r--r--pretyping/tacred.ml4
-rw-r--r--pretyping/typing.ml6
19 files changed, 211 insertions, 184 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c2c8065a98..efab5b9779 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -70,7 +70,7 @@ let error_wrong_numarg_inductive ?loc env c n =
let list_try_compile f l =
let rec aux errors = function
- | [] -> if errors = [] then anomaly (str "try_find_f") else iraise (List.last errors)
+ | [] -> if errors = [] then anomaly (str "try_find_f.") else iraise (List.last errors)
| h::t ->
try f h
with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e ->
@@ -162,9 +162,9 @@ let feed_history arg = function
| Continuation (n, l, h) when n>=1 ->
Continuation (n-1, arg :: l, h)
| Continuation (n, _, _) ->
- anomaly (str "Bad number of expected remaining patterns: " ++ int n)
+ anomaly (str "Bad number of expected remaining patterns: " ++ int n ++ str ".")
| Result _ ->
- anomaly (Pp.str "Exhausted pattern history")
+ anomaly (Pp.str "Exhausted pattern history.")
(* This is for non exhaustive error message *)
@@ -190,7 +190,7 @@ let pop_history_pattern = function
| Continuation (0, l, MakeConstructor (pci, rh)) ->
feed_history (CAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh
| _ ->
- anomaly (Pp.str "Constructor not yet filled with its arguments")
+ anomaly (Pp.str "Constructor not yet filled with its arguments.")
let pop_history h =
feed_history (CAst.make @@ PatVar Anonymous) h
@@ -425,7 +425,7 @@ let lift_tomatch_type n = liftn_tomatch_type n 1
let current_pattern eqn =
match eqn.patterns with
| pat::_ -> pat
- | [] -> anomaly (Pp.str "Empty list of patterns")
+ | [] -> anomaly (Pp.str "Empty list of patterns.")
let alias_of_pat = CAst.with_val (function
| PatVar name -> name
@@ -438,7 +438,7 @@ let remove_current_pattern eqn =
{ eqn with
patterns = pats;
alias_stack = alias_of_pat pat :: eqn.alias_stack }
- | [] -> anomaly (Pp.str "Empty list of patterns")
+ | [] -> anomaly (Pp.str "Empty list of patterns.")
let push_current_pattern (cur,ty) eqn =
match eqn.patterns with
@@ -447,7 +447,7 @@ let push_current_pattern (cur,ty) eqn =
{ eqn with
rhs = { eqn.rhs with rhs_env = rhs_env };
patterns = pats }
- | [] -> anomaly (Pp.str "Empty list of patterns")
+ | [] -> anomaly (Pp.str "Empty list of patterns.")
(* spiwack: like [push_current_pattern] but does not introduce an
alias in rhs_env. Aliasing binders are only useful for variables at
@@ -457,7 +457,7 @@ let push_noalias_current_pattern eqn =
match eqn.patterns with
| _::pats ->
{ eqn with patterns = pats }
- | [] -> anomaly (Pp.str "push_noalias_current_pattern: Empty list of patterns")
+ | [] -> anomaly (Pp.str "push_noalias_current_pattern: Empty list of patterns.")
@@ -641,7 +641,7 @@ let replace_tomatch sigma n c =
| Pushed (initial,((b,tm),l,na)) :: rest ->
let b = replace_term sigma n c depth b in
let tm = map_tomatch_type (replace_term sigma n c depth) tm in
- List.iter (fun i -> if Int.equal i (n + depth) then anomaly (Pp.str "replace_tomatch")) l;
+ List.iter (fun i -> if Int.equal i (n + depth) then anomaly (Pp.str "replace_tomatch.")) l;
Pushed (initial,((b,tm),l,na)) :: replrec depth rest
| Alias (initial,(na,b,d)) :: rest ->
(* [b] is out of replacement scope *)
@@ -731,7 +731,7 @@ let get_names env sigma sign eqns =
(fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid))
d na
in
- (na::l,(out_name na)::avoid))
+ (na::l,(Name.get_id na)::avoid))
([],allvars) (List.rev sign) names2 in
names3,aliasname
@@ -882,7 +882,7 @@ let specialize_predicate_var (cur,typ,dep) env tms ccl =
(*****************************************************************************)
let generalize_predicate sigma (names,na) ny d tms ccl =
let () = match na with
- | Anonymous -> anomaly (Pp.str "Undetected dependency")
+ | Anonymous -> anomaly (Pp.str "Undetected dependency.")
| _ -> () in
let p = List.length names + 1 in
let ccl = lift_predicate 1 ccl tms in
@@ -1708,7 +1708,7 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
evdref := evd;
(t,tt) in
let b = e_cumul env evdref tt (mkSort s) (* side effect *) in
- if not b then anomaly (Pp.str "Build_tycon: should be a type");
+ if not b then anomaly (Pp.str "Build_tycon: should be a type.");
{ uj_val = t; uj_type = tt }
(* For a multiple pattern-matching problem Xi on t1..tn with return
@@ -1872,7 +1872,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
if not (eq_ind ind ind') then
user_err ?loc (str "Wrong inductive type.");
if not (Int.equal nrealargs_ctxt (List.length realnal)) then
- anomaly (Pp.str "Ill-formed 'in' clause in cases");
+ anomaly (Pp.str "Ill-formed 'in' clause in cases.");
List.rev realnal
| None -> List.make nrealargs_ctxt Anonymous in
LocalAssum (na, EConstr.of_constr (build_dependent_inductive env0 indf'))
@@ -2064,8 +2064,8 @@ let mk_JMeq evdref typ x typ' y =
let mk_JMeq_refl evdref typ x =
papp evdref coq_JMeq_refl [| typ; x |]
-let hole = CAst.make @@
- GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false),
+let hole na = CAst.make @@
+ GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na),
Misctypes.IntroAnonymous, None)
let constr_of_pat env evdref arsign pat avoid =
@@ -2168,7 +2168,7 @@ let vars_of_ctx sigma ctx =
prev,
(CAst.make @@ GApp (
(CAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)),
- [hole; CAst.make @@ GVar prev])) :: vars
+ [hole na; CAst.make @@ GVar prev])) :: vars
| _ ->
match RelDecl.get_name decl with
Anonymous -> invalid_arg "vars_of_ctx"
@@ -2223,14 +2223,14 @@ let build_ineqs evdref prevpatterns pats liftsign =
(Some ([], 0, 0, [])) eqnpats pats
in match acc with
None -> c
- | Some (sign, len, _, c') ->
- let conj = it_mkProd_or_LetIn (mk_coq_not (mk_coq_and c'))
- (lift_rel_context liftsign sign)
- in
- conj :: c)
+ | Some (sign, len, _, c') ->
+ let sigma, conj = mk_coq_and !evdref c' in
+ let sigma, neg = mk_coq_not sigma conj in
+ let conj = it_mkProd_or_LetIn neg (lift_rel_context liftsign sign) in
+ evdref := sigma; conj :: c)
[] prevpatterns
in match diffs with [] -> None
- | _ -> Some (mk_coq_and diffs)
+ | _ -> Some (let sigma, conj = mk_coq_and !evdref diffs in evdref := sigma; conj)
let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
let i = ref 0 in
@@ -2301,7 +2301,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
| l -> CAst.make @@ GApp (bref, l)
in
let branch = match ineqs with
- Some _ -> CAst.make @@ GApp (branch, [ hole ])
+ Some _ -> CAst.make @@ GApp (branch, [ hole Anonymous ])
| None -> branch
in
incr i;
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3ef17912f7..1282e3cb86 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -67,7 +67,7 @@ let apply_coercion_args env evd check isproj argl funj =
if check && not (e_cumul env evdref (Retyping.get_type_of env !evdref h) c1) then
raise NoCoercion;
apply_rec (h::acc) (subst1 h c2) restl
- | _ -> anomaly (Pp.str "apply_coercion_args")
+ | _ -> anomaly (Pp.str "apply_coercion_args.")
in
let res = apply_rec [] funj.uj_type argl in
!evdref, res
@@ -90,8 +90,8 @@ let inh_pattern_coerce_to ?loc env pat ind1 ind2 =
open Program
-let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) env evdref c =
- let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in
+let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c =
+ let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in
Evarutil.e_new_evar env evdref ~src c
let app_opt env evdref f t =
@@ -181,7 +181,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in
let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in
let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in
- let evar = make_existential ?loc env evdref eq in
+ let evar = make_existential ?loc n env evdref eq in
let eq_app x = papp evdref coq_eq_rect
[| eqT; hdx; pred; x; hdy; evar|]
in
@@ -324,7 +324,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
Some
(fun x ->
let cx = app_opt env evdref c x in
- let evar = make_existential ?loc env evdref (mkApp (p, [| cx |]))
+ let evar = make_existential ?loc Anonymous env evdref (mkApp (p, [| cx |]))
in
(papp evdref sig_intro [| u; p; cx; evar |]))
| None ->
@@ -368,7 +368,7 @@ let apply_coercion env sigma p hj typ_cl =
(hj,typ_cl,sigma) p
in evd, j
with NoCoercion as e -> raise e
- | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion")
+ | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion.")
(* Try to coerce to a funclass; raise NoCoercion if not possible *)
let inh_app_fun_core env evd j =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 752819aa39..c93b1e568c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -425,7 +425,7 @@ type binder_kind = BProd | BLambda | BLetIn
(**********************************************************************)
(* Main detyping function *)
-let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable"))
+let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable."))
let set_detype_anonymous f = detype_anonymous := f
let detype_level sigma l =
@@ -907,8 +907,7 @@ let simple_cases_matrix_of_branches ind brs =
let nal,c = it_destRLambda_or_LetIn_names n b in
let mkPatVar na = CAst.make @@ PatVar na in
let p = CAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in
- let map name = try Some (Nameops.out_name name) with Failure _ -> None in
- let ids = List.map_filter map nal in
+ let ids = List.map_filter Nameops.Name.to_option nal in
Loc.tag @@ (ids,[p],c))
brs
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index bf62cea6b6..1d6b611da4 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -638,7 +638,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(fun i ->
let b = nf_evar i b1 in
let t = nf_evar i t1 in
- let na = Nameops.name_max na1 na2 in
+ let na = Nameops.Name.pick na1 na2 in
evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2);
(fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
and f2 i =
@@ -755,7 +755,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
[(fun i -> evar_conv_x ts env i CONV c1 c2);
(fun i ->
let c = nf_evar i c1 in
- let na = Nameops.name_max na1 na2 in
+ let na = Nameops.Name.pick na1 na2 in
evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)]
| Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
@@ -816,7 +816,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
[(fun i -> evar_conv_x ts env i CONV c1 c2);
(fun i ->
let c = nf_evar i c1 in
- let na = Nameops.name_max n1 n2 in
+ let na = Nameops.Name.pick n1 n2 in
evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)]
| Rel x1, Rel x2 ->
@@ -1088,7 +1088,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
let filter' = filter_possible_projections evd c ty ctxt args in
(id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl)
| _, _, [] -> []
- | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list") in
+ | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.") in
let rec set_holes evdref rhs = function
| (id,_,c,cty,evsref,filter,occs)::subst ->
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 98e71c7fd9..de5a627266 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -634,7 +634,7 @@ let make_projectable_subst aliases sigma evi args =
cstrs)
| _ ->
(rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs))
- | _ -> anomaly (Pp.str "Instance does not match its signature"))
+ | _ -> anomaly (Pp.str "Instance does not match its signature."))
sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in
(full_subst,cstr_subst)
@@ -828,7 +828,7 @@ let rec find_projectable_vars with_evars aliases sigma y subst =
| _ -> subst'
end
| [] -> subst'
- | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance")
+ | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance.")
else
subst' in
Id.Map.fold is_projectable subst []
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 923d7d9388..e53d19b595 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -12,6 +12,7 @@ open Nameops
open Globnames
open Misctypes
open Glob_term
+open Evar_kinds
(* Untyped intermediate terms, after ASTs and before constr. *)
@@ -33,109 +34,108 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) =
(na,k,comp1,comp2)
let binding_kind_eq bk1 bk2 = match bk1, bk2 with
-| Decl_kinds.Explicit, Decl_kinds.Explicit -> true
-| Decl_kinds.Implicit, Decl_kinds.Implicit -> true
-| _ -> false
+ | Decl_kinds.Explicit, Decl_kinds.Explicit -> true
+ | Decl_kinds.Implicit, Decl_kinds.Implicit -> true
+ | (Decl_kinds.Explicit | Decl_kinds.Implicit), _ -> false
let case_style_eq s1 s2 = match s1, s2 with
-| LetStyle, LetStyle -> true
-| IfStyle, IfStyle -> true
-| LetPatternStyle, LetPatternStyle -> true
-| MatchStyle, MatchStyle -> true
-| RegularStyle, RegularStyle -> true
-| _ -> false
+ | LetStyle, LetStyle -> true
+ | IfStyle, IfStyle -> true
+ | LetPatternStyle, LetPatternStyle -> true
+ | MatchStyle, MatchStyle -> true
+ | RegularStyle, RegularStyle -> true
+ | (LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle), _ -> false
let rec cases_pattern_eq { CAst.v = p1} { CAst.v = p2 } = match p1, p2 with
-| PatVar na1, PatVar na2 -> Name.equal na1 na2
-| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) ->
- eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
- Name.equal na1 na2
-| _ -> false
+ | PatVar na1, PatVar na2 -> Name.equal na1 na2
+ | PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) ->
+ eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
+ Name.equal na1 na2
+ | (PatVar _ | PatCstr _), _ -> false
let cast_type_eq eq t1 t2 = match t1, t2 with
-| CastConv t1, CastConv t2 -> eq t1 t2
-| CastVM t1, CastVM t2 -> eq t1 t2
-| CastCoerce, CastCoerce -> true
-| CastNative t1, CastNative t2 -> eq t1 t2
-| _ -> false
-
-let rec glob_constr_eq { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with
-| GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2
-| GVar id1, GVar id2 -> Id.equal id1 id2
-| GEvar (id1, arg1), GEvar (id2, arg2) ->
- Id.equal id1 id2 &&
- List.equal instance_eq arg1 arg2
-| GPatVar (b1, pat1), GPatVar (b2, pat2) ->
- (b1 : bool) == b2 && Id.equal pat1 pat2
-| GApp (f1, arg1), GApp (f2, arg2) ->
- glob_constr_eq f1 f2 && List.equal glob_constr_eq arg1 arg2
-| GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) ->
- Name.equal na1 na2 && binding_kind_eq bk1 bk2 &&
- glob_constr_eq t1 t2 && glob_constr_eq c1 c2
-| GProd (na1, bk1, t1, c1), GProd (na2, bk2, t2, c2) ->
- Name.equal na1 na2 && binding_kind_eq bk1 bk2 &&
- glob_constr_eq t1 t2 && glob_constr_eq c1 c2
-| GLetIn (na1, b1, t1, c1), GLetIn (na2, b2, t2, c2) ->
- Name.equal na1 na2 && glob_constr_eq b1 b2 && Option.equal glob_constr_eq t1 t2 && glob_constr_eq c1 c2
-| GCases (st1, c1, tp1, cl1), GCases (st2, c2, tp2, cl2) ->
- case_style_eq st1 st2 && Option.equal glob_constr_eq c1 c2 &&
- List.equal tomatch_tuple_eq tp1 tp2 &&
- List.equal cases_clause_eq cl1 cl2
-| GLetTuple (na1, (n1, p1), c1, t1), GLetTuple (na2, (n2, p2), c2, t2) ->
- List.equal Name.equal na1 na2 && Name.equal n1 n2 &&
- Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 &&
- glob_constr_eq t1 t2
-| GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) ->
- glob_constr_eq m1 m2 && Name.equal pat1 pat2 &&
- Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 &&
- glob_constr_eq t1 t2
-| GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) ->
- fix_kind_eq kn1 kn2 && Array.equal Id.equal id1 id2 &&
- Array.equal (fun l1 l2 -> List.equal glob_decl_eq l1 l2) decl1 decl2 &&
- Array.equal glob_constr_eq c1 c2 &&
- Array.equal glob_constr_eq t1 t2
-| GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2
-| GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) ->
- Option.equal (==) gn1 gn2 (** Only thing sensible *) &&
- Miscops.intro_pattern_naming_eq nam1 nam2
-| GCast (c1, t1), GCast (c2, t2) ->
- glob_constr_eq c1 c2 && cast_type_eq glob_constr_eq t1 t2
-| _ -> false
-
-and tomatch_tuple_eq (c1, p1) (c2, p2) =
+ | CastConv t1, CastConv t2 -> eq t1 t2
+ | CastVM t1, CastVM t2 -> eq t1 t2
+ | CastCoerce, CastCoerce -> true
+ | CastNative t1, CastNative t2 -> eq t1 t2
+ | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> false
+
+let matching_var_kind_eq k1 k2 = match k1, k2 with
+| FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2
+| SecondOrderPatVar id1, SecondOrderPatVar id2 -> Id.equal id1 id2
+| (FirstOrderPatVar _ | SecondOrderPatVar _), _ -> false
+
+let tomatch_tuple_eq f (c1, p1) (c2, p2) =
let eqp (_, (i1, na1)) (_, (i2, na2)) =
eq_ind i1 i2 && List.equal Name.equal na1 na2
in
let eq_pred (n1, o1) (n2, o2) = Name.equal n1 n2 && Option.equal eqp o1 o2 in
- glob_constr_eq c1 c2 && eq_pred p1 p2
+ f c1 c2 && eq_pred p1 p2
-and cases_clause_eq (_, (id1, p1, c1)) (_, (id2, p2, c2)) =
- List.equal Id.equal id1 id2 && List.equal cases_pattern_eq p1 p2 &&
- glob_constr_eq c1 c2
+and cases_clause_eq f (_, (id1, p1, c1)) (_, (id2, p2, c2)) =
+ List.equal Id.equal id1 id2 && List.equal cases_pattern_eq p1 p2 && f c1 c2
-and glob_decl_eq (na1, bk1, c1, t1) (na2, bk2, c2, t2) =
+let glob_decl_eq f (na1, bk1, c1, t1) (na2, bk2, c2, t2) =
Name.equal na1 na2 && binding_kind_eq bk1 bk2 &&
- Option.equal glob_constr_eq c1 c2 &&
- glob_constr_eq t1 t2
-
-and fix_kind_eq k1 k2 = match k1, k2 with
-| GFix (a1, i1), GFix (a2, i2) ->
- let eq (i1, o1) (i2, o2) =
- Option.equal Int.equal i1 i2 && fix_recursion_order_eq o1 o2
- in
- Int.equal i1 i2 && Array.equal eq a1 a1
-| GCoFix i1, GCoFix i2 -> Int.equal i1 i2
-| _ -> false
-
-and fix_recursion_order_eq o1 o2 = match o1, o2 with
-| GStructRec, GStructRec -> true
-| GWfRec c1, GWfRec c2 -> glob_constr_eq c1 c2
-| GMeasureRec (c1, o1), GMeasureRec (c2, o2) ->
- glob_constr_eq c1 c2 && Option.equal glob_constr_eq o1 o2
-| _ -> false
-
-and instance_eq (x1,c1) (x2,c2) =
- Id.equal x1 x2 && glob_constr_eq c1 c2
+ Option.equal f c1 c2 && f t1 t2
+
+let fix_recursion_order_eq f o1 o2 = match o1, o2 with
+ | GStructRec, GStructRec -> true
+ | GWfRec c1, GWfRec c2 -> f c1 c2
+ | GMeasureRec (c1, o1), GMeasureRec (c2, o2) ->
+ f c1 c2 && Option.equal f o1 o2
+ | (GStructRec | GWfRec _ | GMeasureRec _), _ -> false
+
+let fix_kind_eq f k1 k2 = match k1, k2 with
+ | GFix (a1, i1), GFix (a2, i2) ->
+ let eq (i1, o1) (i2, o2) =
+ Option.equal Int.equal i1 i2 && fix_recursion_order_eq f o1 o2
+ in
+ Int.equal i1 i2 && Array.equal eq a1 a1
+ | GCoFix i1, GCoFix i2 -> Int.equal i1 i2
+ | (GFix _ | GCoFix _), _ -> false
+
+let instance_eq f (x1,c1) (x2,c2) =
+ Id.equal x1 x2 && f c1 c2
+
+let mk_glob_constr_eq f { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with
+ | GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2
+ | GVar id1, GVar id2 -> Id.equal id1 id2
+ | GEvar (id1, arg1), GEvar (id2, arg2) ->
+ Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2
+ | GPatVar k1, GPatVar k2 -> matching_var_kind_eq k1 k2
+ | GApp (f1, arg1), GApp (f2, arg2) ->
+ f f1 f2 && List.equal f arg1 arg2
+ | GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) ->
+ Name.equal na1 na2 && binding_kind_eq bk1 bk2 && f t1 t2 && f c1 c2
+ | GProd (na1, bk1, t1, c1), GProd (na2, bk2, t2, c2) ->
+ Name.equal na1 na2 && binding_kind_eq bk1 bk2 && f t1 t2 && f c1 c2
+ | GLetIn (na1, b1, t1, c1), GLetIn (na2, b2, t2, c2) ->
+ Name.equal na1 na2 && f b1 b2 && Option.equal f t1 t2 && f c1 c2
+ | GCases (st1, c1, tp1, cl1), GCases (st2, c2, tp2, cl2) ->
+ case_style_eq st1 st2 && Option.equal f c1 c2 &&
+ List.equal (tomatch_tuple_eq f) tp1 tp2 &&
+ List.equal (cases_clause_eq f) cl1 cl2
+ | GLetTuple (na1, (n1, p1), c1, t1), GLetTuple (na2, (n2, p2), c2, t2) ->
+ List.equal Name.equal na1 na2 && Name.equal n1 n2 &&
+ Option.equal f p1 p2 && f c1 c2 && f t1 t2
+ | GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) ->
+ f m1 m2 && Name.equal pat1 pat2 &&
+ Option.equal f p1 p2 && f c1 c2 && f t1 t2
+ | GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) ->
+ fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 &&
+ Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 &&
+ Array.equal f c1 c2 && Array.equal f t1 t2
+ | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2
+ | GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) ->
+ Option.equal (==) gn1 gn2 (** Only thing sensible *) &&
+ Miscops.intro_pattern_naming_eq nam1 nam2
+ | GCast (c1, t1), GCast (c2, t2) ->
+ f c1 c2 && cast_type_eq f t1 t2
+ | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ |
+ GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _), _ -> false
+
+let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
let map_glob_constr_left_to_right f = CAst.map (function
| GApp (g,args) ->
@@ -215,20 +215,20 @@ let fold_glob_constr f acc = CAst.with_val (function
)
let fold_return_type_with_binders f g v acc (na,tyopt) =
- Option.fold_left (f (name_fold g na v)) acc tyopt
+ Option.fold_left (f (Name.fold_right g na v)) acc tyopt
let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function
| GVar _ -> acc
| GApp (c,args) -> List.fold_left (f v) (f v acc c) args
| GLambda (na,_,b,c) | GProd (na,_,b,c) ->
- f (name_fold g na v) (f v acc b) c
+ f (Name.fold_right g na v) (f v acc b) c
| GLetIn (na,b,t,c) ->
- f (name_fold g na v) (Option.fold_left (f v) (f v acc b) t) c
+ f (Name.fold_right g na v) (Option.fold_left (f v) (f v acc b) t) c
| GCases (_,rtntypopt,tml,pl) ->
let fold_pattern acc (_,(idl,p,c)) = f (List.fold_right g idl v) acc c in
let fold_tomatch (v',acc) (tm,(na,onal)) =
- (Option.fold_left (fun v'' (_,(_,nal)) -> List.fold_right (name_fold g) nal v'')
- (name_fold g na v') onal,
+ (Option.fold_left (fun v'' (_,(_,nal)) -> List.fold_right (Name.fold_right g) nal v'')
+ (Name.fold_right g na v') onal,
f v acc tm) in
let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in
let acc = Option.fold_left (f v') acc rtntypopt in
@@ -242,7 +242,7 @@ let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function
let v,acc =
List.fold_left
(fun (v,acc) (na,k,bbd,bty) ->
- (name_fold g na v, f v (Option.fold_left (f v) acc bbd) bty))
+ (Name.fold_right g na v, f v (Option.fold_left (f v) acc bbd) bty))
(v,acc)
bll.(i) in
f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in
@@ -371,12 +371,12 @@ let loc_of_glob_constr c = c.CAst.loc
let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l
let test_id l id = if collide_id l id then raise Not_found
-let test_na l na = name_iter (test_id l) na
+let test_na l na = Name.iter (test_id l) na
let update_subst na l =
let in_range id l = List.exists (fun (_,id') -> Id.equal id id') l in
- let l' = name_fold Id.List.remove_assoc na l in
- name_fold
+ let l' = Name.fold_right Id.List.remove_assoc na l in
+ Name.fold_right
(fun id _ ->
if in_range id l' then
let id' = Namegen.next_ident_away_from id (fun id' -> in_range id' l') in
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index aa48516aff..f7cc08ca21 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -36,6 +36,9 @@ val map_glob_constr_left_to_right :
val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit
+val mk_glob_constr_eq : (glob_constr -> glob_constr -> bool) ->
+ glob_constr -> glob_constr -> bool
+
val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b
val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index c4a74d990b..8a902f3a33 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -296,7 +296,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
process_constr (push_rel d env) (i+1) (lift 1 f)
(cprest,rest))
| [],[] -> f
- | _,[] | [],_ -> anomaly (Pp.str "process_constr")
+ | _,[] | [],_ -> anomaly (Pp.str "process_constr.")
in
process_constr env 0 f (List.rev cstr.cs_args, recargs)
@@ -533,7 +533,7 @@ let weaken_sort_scheme env evd set sort npars term ty =
mkProd (n, t, c'), mkLambda (n, t, term')
| LetIn (n,b,t,c) -> let c',term' = drec np c in
mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term')
- | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type")
+ | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type.")
in
let ty, term = drec npars ty in
!evdref, ty, term
@@ -577,7 +577,7 @@ let build_mutual_induction_scheme env sigma = function
in
let _ = check_arities env listdepkind in
mis_make_indrec env sigma listdepkind mib u
- | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types")
+ | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types.")
let build_induction_scheme env sigma pind dep kind =
let (mib,mip) = lookup_mind_specif env (fst pind) in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 7f3bafc685..d8252ea9bb 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -538,7 +538,7 @@ let is_predicate_explicitly_dep env sigma pred arsign =
| Name _ -> true
end
- | _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate")
+ | _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate.")
in
srec env (EConstr.of_constr pred) arsign
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 211ffbe01e..e555742bca 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -84,7 +84,7 @@ let concrete_clause_of enum_hyps cl =
(** Miscellaneous functions *)
let out_arg = function
- | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable")
+ | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.")
| Misctypes.ArgArg x -> x
let occurrences_of_hyp id cls =
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index afaa20b6f6..61118cf777 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -139,7 +139,7 @@ let type_of_var env id =
let open Context.Named.Declaration in
try env |> lookup_named id |> get_type
with Not_found ->
- anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound")
+ anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound.")
let sort_of_product env domsort rangsort =
match (domsort, rangsort) with
@@ -405,7 +405,7 @@ let native_norm env sigma c ty =
let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in
if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
EConstr.of_constr res
- | _ -> anomaly (Pp.str "Compilation failure")
+ | _ -> anomaly (Pp.str "Compilation failure.")
let native_conv_generic pb sigma t =
Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 1c8ad0cddd..db2e5da957 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -112,14 +112,14 @@ let rec head_pattern_bound t =
-> raise BoundPattern
(* Perhaps they were arguments, but we don't beta-reduce *)
| PLambda _ -> raise BoundPattern
- | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type")
+ | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.")
let head_of_constr_reference sigma c = match EConstr.kind sigma c with
| Const (sp,_) -> ConstRef sp
| Construct (sp,_) -> ConstructRef sp
| Ind (sp,_) -> IndRef sp
| Var id -> VarRef id
- | _ -> anomaly (Pp.str "Not a rigid reference")
+ | _ -> anomaly (Pp.str "Not a rigid reference.")
let pattern_of_constr env sigma t =
let rec pattern_of_constr env t =
@@ -143,7 +143,7 @@ let pattern_of_constr env sigma t =
match kind_of_term f with
| Evar (evk,args) ->
(match snd (Evd.evar_source evk sigma) with
- Evar_kinds.MatchingVar (true,id) -> Some id
+ Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id
| _ -> None)
| _ -> None
with
@@ -156,13 +156,14 @@ let pattern_of_constr env sigma t =
pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) []))
| Evar (evk,ctxt as ev) ->
(match snd (Evd.evar_source evk sigma) with
- | Evar_kinds.MatchingVar (b,id) ->
- assert (not b); PMeta (Some id)
+ | Evar_kinds.MatchingVar (Evar_kinds.FirstOrderPatVar id) ->
+ PMeta (Some id)
| Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ ->
(* These are the two evar kinds used for existing goals *)
(* see Proofview.mark_in_evm *)
if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev)
else PEvar (evk,Array.map (pattern_of_constr env) ctxt)
+ | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
| _ ->
PMeta None)
| Case (ci,p,a,br) ->
@@ -329,26 +330,26 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
| GVar id ->
(try PRel (List.index Name.equal (Name id) vars)
with Not_found -> PVar id)
- | GPatVar (false,n) ->
+ | GPatVar (Evar_kinds.FirstOrderPatVar n) ->
metas := n::!metas; PMeta (Some n)
| GRef (gr,_) ->
PRef (canonical_gr gr)
(* Hack to avoid rewriting a complete interpretation of patterns *)
- | GApp ({ CAst.v = GPatVar (true,n) }, cl) ->
+ | GApp ({ CAst.v = GPatVar (Evar_kinds.SecondOrderPatVar n) }, cl) ->
metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
| GApp (c,cl) ->
PApp (pat_of_raw metas vars c,
Array.of_list (List.map (pat_of_raw metas vars) cl))
| GLambda (na,bk,c1,c2) ->
- name_iter (fun n -> metas := n::!metas) na;
+ Name.iter (fun n -> metas := n::!metas) na;
PLambda (na, pat_of_raw metas vars c1,
pat_of_raw metas (na::vars) c2)
| GProd (na,bk,c1,c2) ->
- name_iter (fun n -> metas := n::!metas) na;
+ Name.iter (fun n -> metas := n::!metas) na;
PProd (na, pat_of_raw metas vars c1,
pat_of_raw metas (na::vars) c2)
| GLetIn (na,c1,t,c2) ->
- name_iter (fun n -> metas := n::!metas) na;
+ Name.iter (fun n -> metas := n::!metas) na;
PLetIn (na, pat_of_raw metas vars c1,
Option.map (pat_of_raw metas vars) t,
pat_of_raw metas (na::vars) c2)
@@ -411,7 +412,7 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
and pats_of_glob_branches loc metas vars ind brs =
let get_arg = function
| { CAst.v = PatVar na } ->
- name_iter (fun n -> metas := n::!metas) na;
+ Name.iter (fun n -> metas := n::!metas) na;
na
| { CAst.v = PatCstr(_,_,_) ; loc } -> err ?loc (Pp.str "Non supported pattern.")
in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e72394fa28..08a6dd4dbd 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -199,7 +199,7 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) =
let names, _ = Global.global_universe_names () in
if CString.string_contains ~where:s ~what:"." then
match List.rev (CString.split '.' s) with
- | [] -> anomaly (str"Invalid universe name " ++ str s)
+ | [] -> anomaly (str"Invalid universe name " ++ str s ++ str".")
| n :: dp ->
let num = int_of_string n in
let dp = DirPath.make (List.map Id.of_string dp) in
@@ -383,6 +383,21 @@ let process_inference_flags flags env initial_sigma (sigma,c) =
let c = if flags.expand_evars then nf_evar sigma c else c in
sigma,c
+let adjust_evar_source evdref na c =
+ match na, kind !evdref c with
+ | Name id, Evar (evk,args) ->
+ let evi = Evd.find !evdref evk in
+ begin match evi.evar_source with
+ | loc, Evar_kinds.QuestionMark (b,Anonymous) ->
+ let src = (loc,Evar_kinds.QuestionMark (b,na)) in
+ let sigma = Sigma.Unsafe.of_evar_map !evdref in
+ let Sigma (evk', evd, _) = restrict_evar sigma evk (evar_filter evi) ~src None in
+ evdref := Sigma.to_evar_map evd;
+ mkEvar (evk',args)
+ | _ -> c
+ end
+ | _, _ -> c
+
(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
let allow_anonymous_refs = ref false
@@ -610,13 +625,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in
inh_conv_coerce_to_tycon ?loc env evdref j tycon
- | GPatVar (someta,n) ->
+ | GPatVar kind ->
let env = ltac_interp_name_env k0 lvar env !evdref in
let ty =
match tycon with
| Some ty -> ty
| None -> new_type_evar env evdref loc in
- let k = Evar_kinds.MatchingVar (someta,n) in
+ let k = Evar_kinds.MatchingVar kind in
{ uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
| GHole (k, naming, None) ->
@@ -785,6 +800,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
args, nf_evar !evdref (j_val hj)
else [], j_val hj
in
+ let ujval = adjust_evar_source evdref na ujval in
let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in
let j = { uj_val = value; uj_type = typ } in
apply_rec env (n+1) j candargs rest
@@ -1133,7 +1149,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
| Sort s -> ESorts.kind sigma s
| Evar ev when is_Type (existential_type sigma ev) ->
evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev
- | _ -> anomaly (Pp.str "Found a type constraint which is not a type")
+ | _ -> anomaly (Pp.str "Found a type constraint which is not a type.")
in
{ utj_val = v;
utj_type = s }
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 8769c5659e..2fa3facb30 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -9,7 +9,6 @@
open CErrors
open Util
-let init_constant dir s () = Universes.constr_of_global @@ Coqlib.coq_reference "Program" dir s
let init_reference dir s () = Coqlib.coq_reference "Program" dir s
let papp evdref r args =
@@ -39,20 +38,25 @@ let coq_eq_rect = init_reference ["Init"; "Logic"] "eq_rect"
let coq_JMeq_ind = init_reference ["Logic";"JMeq"] "JMeq"
let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl"
-let coq_not = init_constant ["Init";"Logic"] "not"
-let coq_and = init_constant ["Init";"Logic"] "and"
+let coq_not = init_reference ["Init";"Logic"] "not"
+let coq_and = init_reference ["Init";"Logic"] "and"
-let delayed_force c = EConstr.of_constr (c ())
+let new_global sigma gr =
+ let open Sigma in
+ let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr
+ in Sigma.to_evar_map sigma, c
-let mk_coq_not x = EConstr.mkApp (delayed_force coq_not, [| x |])
+let mk_coq_not sigma x =
+ let sigma, notc = new_global sigma (coq_not ()) in
+ sigma, EConstr.mkApp (notc, [| x |])
let unsafe_fold_right f = function
hd :: tl -> List.fold_right f tl hd
| [] -> invalid_arg "unsafe_fold_right"
-let mk_coq_and l =
- let and_typ = delayed_force coq_and in
- unsafe_fold_right
+let mk_coq_and sigma l =
+ let sigma, and_typ = new_global sigma (coq_and ()) in
+ sigma, unsafe_fold_right
(fun c conj ->
EConstr.mkApp (and_typ, [| c ; conj |]))
l
diff --git a/pretyping/program.mli b/pretyping/program.mli
index 94a7bdcb6d..8439b9528c 100644
--- a/pretyping/program.mli
+++ b/pretyping/program.mli
@@ -32,8 +32,8 @@ val coq_eq_rect : unit -> global_reference
val coq_JMeq_ind : unit -> global_reference
val coq_JMeq_refl : unit -> global_reference
-val mk_coq_and : constr list -> constr
-val mk_coq_not : constr -> constr
+val mk_coq_and : Evd.evar_map -> constr list -> Evd.evar_map * constr
+val mk_coq_not : Evd.evar_map -> constr -> Evd.evar_map * constr
(** Polymorphic application of delayed references *)
val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e7c9635829..c976fe66dd 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1317,19 +1317,23 @@ let sigma_univ_state =
let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
?(ts=full_transparent_state) env sigma x y =
(** FIXME *)
+ let open Universes in
let x = EConstr.Unsafe.to_constr x in
let y = EConstr.Unsafe.to_constr y in
try
- let fold cstr sigma =
- try Some (Evd.add_universe_constraints sigma cstr)
- with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None
- in
+ let fold cstr accu = Some (Constraints.fold Constraints.add cstr accu) in
let b, sigma =
let ans =
if pb == Reduction.CUMUL then
- Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y sigma
+ Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty
else
- Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y sigma
+ Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty
+ in
+ let ans = match ans with
+ | None -> None
+ | Some cstr ->
+ try Some (Evd.add_universe_constraints sigma cstr)
+ with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None
in
match ans with
| None -> false, sigma
@@ -1441,7 +1445,7 @@ let instance sigma s c =
let hnf_prod_app env sigma t n =
match EConstr.kind sigma (whd_all env sigma t) with
| Prod (_,_,b) -> subst1 n b
- | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
+ | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.")
let hnf_prod_appvect env sigma t nl =
Array.fold_left (fun acc t -> hnf_prod_app env sigma acc t) t nl
@@ -1452,7 +1456,7 @@ let hnf_prod_applist env sigma t nl =
let hnf_lam_app env sigma t n =
match EConstr.kind sigma (whd_all env sigma t) with
| Lambda (_,_,b) -> subst1 n b
- | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction")
+ | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction.")
let hnf_lam_appvect env sigma t nl =
Array.fold_left (fun acc t -> hnf_lam_app env sigma acc t) t nl
@@ -1689,5 +1693,5 @@ let betazetaevar_applist sigma n c l =
| Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
| LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
| Evar _, _ -> applist (substl env t, stack)
- | _ -> anomaly (Pp.str "Not enough lambda/let's") in
+ | _ -> anomaly (Pp.str "Not enough lambda/let's.") in
stacklam n [] c l
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 496c706ec6..a1d0977f5a 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -48,7 +48,7 @@ let retype_error re = raise (RetypeError re)
let anomaly_on_error f x =
try f x
- with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e)
+ with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e ++ str ".")
let get_type_from_constraints env sigma t =
if isEvar sigma (fst (decompose_app_vect sigma t)) then
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 3d41d2ddd5..f2b0995b0b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -107,7 +107,7 @@ let destEvalRefU sigma c = match EConstr.kind sigma c with
| Var id -> (EvalVar id, EInstance.empty)
| Rel n -> (EvalRel n, EInstance.empty)
| Evar ev -> (EvalEvar ev, EInstance.empty)
- | _ -> anomaly (Pp.str "Not an unfoldable reference")
+ | _ -> anomaly (Pp.str "Not an unfoldable reference.")
let unsafe_reference_opt_value env sigma eval =
match eval with
@@ -307,7 +307,7 @@ let compute_consteval_mutual_fix env sigma ref =
(* Forget all \'s and args and do as if we had started with c' *)
let ref,_ = destEvalRefU sigma c' in
(match unsafe_reference_opt_value env sigma ref with
- | None -> anomaly (Pp.str "Should have been trapped by compute_direct")
+ | None -> anomaly (Pp.str "Should have been trapped by compute_direct.")
| Some c -> srec env (minarg-nargs) [] ref c)
| _ -> (* Should not occur *) NotAnElimination
in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 757e12451e..7ad988ad0b 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -31,7 +31,7 @@ let push_rec_types pfix env =
let meta_type evd mv =
let ty =
try Evd.meta_ftype evd mv
- with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv)) in
+ with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in
let ty = Evd.map_fl EConstr.of_constr ty in
meta_instance evd ty
@@ -121,11 +121,11 @@ let lambda_applist_assum sigma n c l =
let rec app n subst t l =
if Int.equal n 0 then
if l == [] then substl subst t
- else anomaly (Pp.str "Not enough arguments")
+ else anomaly (Pp.str "Not enough arguments.")
else match EConstr.kind sigma t, l with
| Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l
| LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
- | _ -> anomaly (Pp.str "Not enough lambda/let's") in
+ | _ -> anomaly (Pp.str "Not enough lambda/let's.") in
app n [] c l
let e_type_case_branches env evdref (ind,largs) pj c =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 05:27:56 +0000