aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/lemmas.ml8
-rw-r--r--stm/stm.ml4
-rw-r--r--stm/texmacspp.ml12
-rw-r--r--stm/vernac_classifier.ml14
4 files changed, 21 insertions, 17 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index a7ef96c66..7679b1a66 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -212,7 +212,7 @@ let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
let default_thm_id = Id.of_string "Unnamed_thm"
let compute_proof_name locality = function
- | Some (loc,id) ->
+ | Some ((loc,id),pl) ->
(* We check existence here: it's a bit late at Qed time *)
if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
@@ -431,7 +431,11 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
let start_proof_com kind thms hook =
let env0 = Global.env () in
- let evdref = ref (Evd.from_env env0) in
+ let levels = Option.map snd (fst (List.hd thms)) in
+ let evdref = ref (match levels with
+ | None -> Evd.from_env env0
+ | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l))
+ in
let thms = List.map (fun (sopt,(bl,t,guard)) ->
let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
let t', imps' = interp_type_evars_impls ~impls env evdref t in
diff --git a/stm/stm.ml b/stm/stm.ml
index e6271f608..4a303f036 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -424,8 +424,8 @@ end = struct (* {{{ *)
let reachable id = reachable !vcs id
let mk_branch_name { expr = x } = Branch.make
(match x with
- | VernacDefinition (_,(_,i),_) -> string_of_id i
- | VernacStartTheoremProof (_,[Some (_,i),_],_) -> string_of_id i
+ | VernacDefinition (_,((_,i),_),_) -> string_of_id i
+ | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> string_of_id i
| _ -> "branch")
let edit_branch = Branch.make "edit"
let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index aaa6c2c07..fb41bb7be 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -244,7 +244,7 @@ and pp_local_decl_expr lde = (* don't know what it is for now *)
match lde with
| AssumExpr (_, ce) -> pp_expr ce
| DefExpr (_, ce, _) -> pp_expr ce
-and pp_inductive_expr ((_, (l, id)), lbl, ceo, _, cl_or_rdexpr) =
+and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) =
(* inductive_expr *)
let b,e = Loc.unloc l in
let location = ["begin", string_of_int b; "end", string_of_int e] in
@@ -273,7 +273,7 @@ and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
| CMeasureRec (e, None) -> "mesrec", [pp_expr e]
| CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in
Element ("recursion_order", ["kind", kind] @ attrs, expr)
-and pp_fixpoint_expr ((loc, id), (optid, roe), lbl, ce, ceo) =
+and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) =
(* fixpoint_expr *)
let start, stop = unlock loc in
let id = Id.to_string id in
@@ -286,7 +286,7 @@ and pp_fixpoint_expr ((loc, id), (optid, roe), lbl, ce, ceo) =
| Some ce -> [pp_expr ce]
| None -> []
end
-and pp_cofixpoint_expr ((loc, id), lbl, ce, ceo) = (* cofixpoint_expr *)
+and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
(* Nota: it is like fixpoint_expr without (optid, roe)
* so could be merged if there is no more differences *)
let start, stop = unlock loc in
@@ -473,7 +473,7 @@ and pp_expr ?(attr=[]) e =
xmlApply loc
(xmlOperator "fix" loc ::
List.flatten (List.map
- (fun (a,b,cl,c,d) -> pp_fixpoint_expr (a,b,cl,c,Some d))
+ (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d))
fel))
let pp_comment (c) =
@@ -540,7 +540,7 @@ let rec tmpp v loc =
| VernacConstraint _
| VernacPolymorphic (_, _) as x -> xmlTODO loc x
(* Gallina *)
- | VernacDefinition (ldk, (_,id), de) ->
+ | VernacDefinition (ldk, ((_,id),_), de) ->
let l, dk =
match ldk with
| Some l, dk -> (l, dk)
@@ -555,7 +555,7 @@ let rec tmpp v loc =
let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
let str_id = Id.to_string id in
(xmlDef str_dk str_id loc [pp_expr e])
- | VernacStartTheoremProof (tk, [ Some (_,id), ([], statement, None) ], b) ->
+ | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
let str_tk = Kindops.string_of_theorem_kind tk in
let str_id = Id.to_string id in
(xmlThm str_tk str_id loc [pp_expr statement])
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 2b5eb8683..a2b779516 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -116,25 +116,25 @@ let rec classify_vernac e =
| VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
(* StartProof *)
| VernacDefinition (
- (Some Decl_kinds.Discharge,Decl_kinds.Definition),(_,i),ProveBody _) ->
+ (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) ->
VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater
- | VernacDefinition (_,(_,i),ProveBody _) ->
+ | VernacDefinition (_,((_,i),_),ProveBody _) ->
VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
| VernacStartTheoremProof (_,l,_) ->
let ids =
- CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in
+ CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
| VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
| VernacFixpoint (_,l) ->
let ids, open_proof =
- List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) ->
+ List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
else VtSideff ids, VtLater
| VernacCoFixpoint (_,l) ->
let ids, open_proof =
- List.fold_left (fun (l,b) (((_,id),_,_,p),_) ->
+ List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
@@ -143,9 +143,9 @@ let rec classify_vernac e =
| VernacAssumption (_,_,l) ->
let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in
VtSideff ids, VtLater
- | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater
+ | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater
| VernacInductive (_,_,l) ->
- let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with
+ let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with
| Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
| RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
CList.map_filter (function
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 23:18:50 +0000