aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml14
-rw-r--r--vernac/auto_ind_decl.ml6
-rw-r--r--vernac/comDefinition.ml5
-rw-r--r--vernac/comInductive.ml2
-rw-r--r--vernac/declareUniv.ml8
-rw-r--r--vernac/metasyntax.ml8
-rw-r--r--vernac/prettyp.ml2
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/vernacentries.ml94
-rw-r--r--vernac/vernacinterp.ml2
10 files changed, 93 insertions, 50 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 792f07bb89..9c5f111e28 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -176,7 +176,10 @@ let fold_with_full_binders g f n acc c =
| App (c,l) -> Array.fold_left (f n) (f n acc c) l
| Proj (_,c) -> f n acc c
| Evar (_,l) -> List.fold_left (f n) acc l
- | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
+ | Case (ci, u, pms, p, iv, c, bl) ->
+ let mib = lookup_mind (fst ci.ci_ind) in
+ let (ci, p, iv, c, bl) = Inductive.expand_case_specif mib (ci, u, pms, p, iv, c, bl) in
+ Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
| Fix (_,(lna,tl,bl)) ->
let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
@@ -201,12 +204,11 @@ let rec traverse current ctx accu t =
| Construct (((mind, _), _) as cst, _) ->
traverse_inductive accu mind (ConstructRef cst)
| Meta _ | Evar _ -> assert false
-| Case (_,oty,_,c,[||]) ->
+| Case (_, _, _, ([|_|], oty), _, c, [||]) when Vars.noccurn 1 oty ->
(* non dependent match on an inductive with no constructors *)
- begin match Constr.(kind oty, kind c) with
- | Lambda(_,_,oty), Const (kn, _)
- when Vars.noccurn 1 oty &&
- not (Declareops.constant_has_body (lookup_constant kn)) ->
+ begin match Constr.kind c with
+ | Const (kn, _)
+ when not (Declareops.constant_has_body (lookup_constant kn)) ->
let body () = Option.map pi1 (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in
traverse_object
~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn)
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index f715459616..cc59a96834 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -351,13 +351,13 @@ let build_beq_scheme mode kn =
done;
ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a))
- (mkCase (ci,do_predicate rel_list nb_cstr_args,NoInvert,
- mkVar (Id.of_string "Y") ,ar2))
+ (mkCase (Inductive.contract_case env ((ci,do_predicate rel_list nb_cstr_args,
+ NoInvert, mkVar (Id.of_string "Y") ,ar2))))
(constrsi.(i).cs_args))
done;
mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1)) (
mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2)) (
- mkCase (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar)))
+ mkCase (Inductive.contract_case env (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar))))
in (* build_beq_scheme *)
let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and
types = Array.make nb_ind mkSet and
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index c54adb45f9..b3ffb864f2 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -69,9 +69,10 @@ let protect_pattern_in_binder bl c ctypopt =
| LetIn (x,b,t,c) ->
let evd,c = aux (push_rel (LocalDef (x,b,t)) env) evd c in
evd, mkLetIn (x,t,b,c)
- | Case (ci,p,iv,a,bl) ->
+ | Case (ci,u,pms,p,iv,a,bl) ->
+ let (ci, p, iv, a, bl) = EConstr.expand_case env evd (ci, u, pms, p, iv, a, bl) in
let evd,bl = Array.fold_left_map (aux env) evd bl in
- evd, mkCase (ci,p,iv,a,bl)
+ evd, mkCase (EConstr.contract_case env evd (ci, p, iv, a, bl))
| Cast (c,_,_) -> f env evd c (* we remove the cast we had set *)
(* This last case may happen when reaching the proof of an
impossible case, as when pattern-matching on a vector of length 1 *)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 2be6097184..a91771f22d 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -492,7 +492,7 @@ let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams ~binders:k c =
end)
sigma args
| _ -> Termops.fold_constr_with_full_binders
- sigma
+ env sigma
(fun d (env,k) -> EConstr.push_rel d env, k+1)
aux envk sigma c
in
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 834ef0d29a..91ab17575d 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -74,6 +74,10 @@ let input_univ_names : universe_name_decl -> Libobject.obj =
subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
classify_function = (fun a -> Substitute a) }
+let input_univ_names (src, l) =
+ if CList.is_empty l then ()
+ else Lib.add_anonymous_leaf (input_univ_names (src, l))
+
let invent_name (named,cnt) u =
let rec aux i =
let na = Id.of_string ("u"^(string_of_int i)) in
@@ -120,7 +124,7 @@ let declare_univ_binders gr pl =
aux, (id,univ) :: univs)
(LSet.diff levels named) ((pl,0),univs)
in
- Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
+ input_univ_names (QualifiedUniv l, univs)
let do_universe ~poly l =
let in_section = Global.sections_are_opened () in
@@ -134,7 +138,7 @@ let do_universe ~poly l =
Univ.LSet.empty l, Univ.Constraint.empty
in
let src = if poly then BoundUniv else UnqualifiedUniv in
- let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
+ let () = input_univ_names (src, l) in
DeclareUctx.declare_universe_context ~poly ctx
let do_constraint ~poly l =
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index e6244ee3b5..2fe402ff08 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1793,15 +1793,9 @@ let remove_delimiters local scope =
let add_class_scope local scope cl =
Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl))
-(* Check if abbreviation to a name and avoid early insertion of
- maximal implicit arguments *)
-let try_interp_name_alias = function
- | [], { CAst.v = CRef (ref,_) } -> intern_reference ref
- | _ -> raise Not_found
-
let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } =
let acvars,pat,reversibility =
- try Id.Map.empty, NRef (try_interp_name_alias (vars,c)), APrioriReversible
+ try Id.Map.empty, try_interp_name_alias (vars,c), APrioriReversible
with Not_found ->
let fold accu id = Id.Map.add id NtnInternTypeAny accu in
let i_vars = List.fold_left fold Id.Map.empty vars in
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 0fc6c7f87b..79a0cdf8d1 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -947,7 +947,7 @@ let print_about_any ?loc env sigma k udecl =
[hov 0 (str "Expands to: " ++ pr_located_qualid k)])
| Syntactic kn ->
let () = match Syntax_def.search_syntactic_definition kn with
- | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref
+ | [],Notation_term.NRef (ref,_) -> Dumpglob.add_glob ?loc ref
| _ -> () in
v 0 (
print_syntactic_def env kn ++ fnl () ++
diff --git a/vernac/record.ml b/vernac/record.ml
index 68219603b4..96e4a47d2d 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -366,7 +366,7 @@ let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramde
let ci = Inductiveops.make_case_info env indsp rci LetStyle in
(* Record projections are always NoInvert because they're at
constant relevance *)
- mkCase (ci, p, NoInvert, mkRel 1, [|branch|]), None
+ mkCase (Inductive.contract_case env (ci, p, NoInvert, mkRel 1, [|branch|])), None
in
let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e8cb1d65a9..1c774a35bf 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -309,6 +309,17 @@ let print_registered () =
in
hov 0 (prlist_with_sep fnl pr_lib_ref @@ Coqlib.get_lib_refs ())
+let dump_universes output g =
+ let open Univ in
+ let dump_arc u = function
+ | UGraph.Node ltle ->
+ Univ.LMap.iter (fun v strict ->
+ let typ = if strict then Lt else Le in
+ output typ u v) ltle;
+ | UGraph.Alias v ->
+ output Eq u v
+ in
+ Univ.LMap.iter dump_arc g
let dump_universes_gen prl g s =
let output = open_out s in
@@ -342,7 +353,7 @@ let dump_universes_gen prl g s =
in
let output_constraint k l r = output_constraint k (prl l) (prl r) in
try
- UGraph.dump_universes output_constraint g;
+ dump_universes output_constraint g;
close ();
str "Universes written to file \"" ++ str s ++ str "\"."
with reraise ->
@@ -367,13 +378,66 @@ let universe_subgraph ?loc kept univ =
let univ = LSet.fold add kept UGraph.initial_universes in
UGraph.merge_constraints csts univ
+let sort_universes g =
+ let open Univ in
+ let rec normalize u = match LMap.find u g with
+ | UGraph.Alias u -> normalize u
+ | UGraph.Node _ -> u
+ in
+ let get_next u = match LMap.find u g with
+ | UGraph.Alias u -> assert false (* nodes are normalized *)
+ | UGraph.Node ltle -> ltle
+ in
+ (* Compute the longest chain of Lt constraints from Set to any universe *)
+ let rec traverse accu todo = match todo with
+ | [] -> accu
+ | (u, n) :: todo ->
+ let () = assert (Level.equal (normalize u) u) in
+ let n = match LMap.find u accu with
+ | m -> if m < n then Some n else None
+ | exception Not_found -> Some n
+ in
+ match n with
+ | None -> traverse accu todo
+ | Some n ->
+ let accu = LMap.add u n accu in
+ let next = get_next u in
+ let fold v lt todo =
+ let v = normalize v in
+ if lt then (v, n + 1) :: todo else (v, n) :: todo
+ in
+ let todo = LMap.fold fold next todo in
+ traverse accu todo
+ in
+ (* Only contains normalized nodes *)
+ let levels = traverse LMap.empty [normalize Level.set, 0] in
+ let max_level = LMap.fold (fun _ n accu -> max n accu) levels 0 in
+ let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"] in
+ let ulevels = Array.init max_level (fun i -> Level.(make (UGlobal.make dummy_mp i))) in
+ let ulevels = Array.cons Level.set ulevels in
+ (* Add the normal universes *)
+ let fold (cur, ans) u =
+ let ans = LMap.add cur (UGraph.Node (LMap.singleton u true)) ans in
+ (u, ans)
+ in
+ let _, ans = Array.fold_left fold (Level.prop, LMap.empty) ulevels in
+ (* Add alias pointers *)
+ let fold u _ ans =
+ if Level.is_small u then ans
+ else
+ let n = LMap.find (normalize u) levels in
+ LMap.add u (UGraph.Alias ulevels.(n)) ans
+ in
+ LMap.fold fold g ans
+
let print_universes ?loc ~sort ~subgraph dst =
let univ = Global.universes () in
let univ = match subgraph with
| None -> univ
| Some g -> universe_subgraph ?loc g univ
in
- let univ = if sort then UGraph.sort_universes univ else univ in
+ let univ = UGraph.repr univ in
+ let univ = if sort then sort_universes univ else univ in
let pr_remaining =
if Global.is_joined_environment () then mt ()
else str"There may remain asynchronous universe constraints"
@@ -1337,31 +1401,9 @@ let warn_implicit_core_hint_db =
(fun () -> strbrk "Adding and removing hints in the core database implicitly is deprecated. "
++ strbrk"Please specify a hint database.")
-let warn_deprecated_hint_without_locality =
- CWarnings.create ~name:"deprecated-hint-without-locality" ~category:"deprecated"
- (fun () -> strbrk "The default value for hint locality is currently \
- \"local\" in a section and \"global\" otherwise, but is scheduled to change \
- in a future release. For the time being, adding hints outside of sections \
- without specifying an explicit locality is therefore deprecated. It is \
- recommended to use \"export\" whenever possible.")
-
-let check_hint_locality = function
-| OptGlobal ->
- if Global.sections_are_opened () then
- CErrors.user_err Pp.(str
- "This command does not support the global attribute in sections.");
-| OptExport ->
- if Global.sections_are_opened () then
- CErrors.user_err Pp.(str
- "This command does not support the export attribute in sections.");
-| OptDefault ->
- if not @@ Global.sections_are_opened () then
- warn_deprecated_hint_without_locality ()
-| OptLocal -> ()
-
let vernac_remove_hints ~atts dbnames ids =
let locality = Attributes.(parse option_locality atts) in
- let () = check_hint_locality locality in
+ let () = Hints.check_hint_locality locality in
let dbnames =
if List.is_empty dbnames then
(warn_implicit_core_hint_db (); ["core"])
@@ -1376,7 +1418,7 @@ let vernac_hints ~atts dbnames h =
else dbnames
in
let locality, poly = Attributes.(parse Notations.(option_locality ++ polymorphic) atts) in
- let () = check_hint_locality locality in
+ let () = Hints.check_hint_locality locality in
Hints.add_hints ~locality dbnames (ComHints.interp_hints ~poly h)
let vernac_syntactic_definition ~atts lid x only_parsing =
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index e5971e1aaa..3a8a80d25a 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -82,7 +82,7 @@ let vernac_timeout ?timeout (f : 'a -> 'b) (x : 'a) : 'b =
match !default_timeout, timeout with
| _, Some n
| Some n, None ->
- (match Control.timeout n f x with
+ (match Control.timeout (float_of_int n) f x with
| None -> Exninfo.iraise (Exninfo.capture CErrors.Timeout)
| Some x -> x)
| None, None ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 00:54:19 +0000