aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml417
-rw-r--r--vernac/classes.ml5
-rw-r--r--vernac/comArguments.ml11
-rw-r--r--vernac/comFixpoint.ml1
-rw-r--r--vernac/comInductive.ml12
-rw-r--r--vernac/comInductive.mli4
-rw-r--r--vernac/declare.ml40
-rw-r--r--vernac/declare.mli11
-rw-r--r--vernac/metasyntax.ml14
-rw-r--r--vernac/prettyp.ml36
-rw-r--r--vernac/proof_using.ml23
-rw-r--r--vernac/record.ml6
-rw-r--r--vernac/vernacentries.ml28
-rw-r--r--vernac/vernacinterp.ml7
-rw-r--r--vernac/vernacstate.ml7
-rw-r--r--vernac/vernacstate.mli17
16 files changed, 330 insertions, 309 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index f47cdd8bf0..7a7e7d6e35 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -556,11 +556,17 @@ let list_id l = List.fold_left ( fun a decl -> let s' =
Id.of_string (s'^"_lb"))
::a
) [] l
+
+let avoid_of_list_id list_id =
+ List.fold_left (fun avoid (s,seq,sbl,slb) ->
+ List.fold_left (fun avoid id -> Id.Set.add id avoid)
+ avoid [s;seq;sbl;slb])
+ Id.Set.empty list_id
+
(*
build the right eq_I A B.. N eq_A .. eq_N
*)
-let eqI ind l =
- let list_id = list_id l in
+let eqI ind list_id =
let eA = Array.of_list((List.map (fun (s,_,_,_) -> mkVar s) list_id)@
(List.map (fun (_,seq,_,_)-> mkVar seq) list_id ))
and e = match lookup_scheme beq_scheme_kind ind with
@@ -568,7 +574,7 @@ let eqI ind l =
| None ->
user_err ~hdr:"AutoIndDecl.eqI"
(str "The boolean equality on " ++ Printer.pr_inductive (Global.env ()) ind ++ str " is needed.");
- in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA))
+ in mkApp(e,eA)
(**********************************************************************)
(* Boolean->Leibniz *)
@@ -576,12 +582,12 @@ let eqI ind l =
open Namegen
let compute_bl_goal ind lnamesparrec nparrec =
- let eqI = eqI ind lnamesparrec in
let list_id = list_id lnamesparrec in
- let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
+ let eqI = eqI ind list_id in
+ let avoid = avoid_of_list_id list_id in
+ let x = next_ident_away (Id.of_string "x") avoid in
+ let y = next_ident_away (Id.of_string "y") (Id.Set.add x avoid) in
let create_input c =
- let x = next_ident_away (Id.of_string "x") avoid and
- y = next_ident_away (Id.of_string "y") avoid in
let bl_typ = List.map (fun (s,seq,_,_) ->
mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) (
mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) (
@@ -607,88 +613,74 @@ let compute_bl_goal ind lnamesparrec nparrec =
in
mkNamedProd x (RelDecl.get_type decl) a) eq_input lnamesparrec
in
- let n = next_ident_away (Id.of_string "x") avoid and
- m = next_ident_away (Id.of_string "y") avoid in
let u = Univ.Instance.empty in
create_input (
- mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd (ind,u) nparrec) (
- mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) (
+ mkNamedProd (make_annot x Sorts.Relevant) (mkFullInd (ind,u) nparrec) (
+ mkNamedProd (make_annot y Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) (
mkArrow
- (mkApp(eq (),[|bb ();mkApp(eqI,[|mkVar n;mkVar m|]);tt ()|]))
+ (mkApp(eq (),[|bb ();mkApp(eqI,[|mkVar x;mkVar y|]);tt ()|]))
Sorts.Relevant
- (mkApp(eq (),[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|]))
+ (mkApp(eq (),[|mkFullInd (ind,u) (nparrec+3);mkVar x;mkVar y|]))
)))
let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
let list_id = list_id lnamesparrec in
- let avoid = ref [] in
- let first_intros =
- ( List.map (fun (s,_,_,_) -> s ) list_id ) @
- ( List.map (fun (_,seq,_,_ ) -> seq) list_id ) @
- ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id )
- in
- let fresh_id s gl =
- let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in
- avoid := fresh::(!avoid); fresh
- in
- Proofview.Goal.enter begin fun gl ->
- let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
- let freshn = fresh_id (Id.of_string "x") gl in
- let freshm = fresh_id (Id.of_string "y") gl in
- let freshz = fresh_id (Id.of_string "Z") gl in
- (* try with *)
- Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros;
- intro_using freshn ;
- induct_on (EConstr.mkVar freshn);
- intro_using freshm;
- destruct_on (EConstr.mkVar freshm);
- intro_using freshz;
- intros;
- Tacticals.New.tclTRY (
- Tacticals.New.tclORELSE reflexivity my_discr_tac
- );
- simpl_in_hyp (freshz,Locus.InHyp);
-(*
+ let first_intros =
+ ( List.map (fun (s,_,_,_) -> s ) list_id )
+ @ ( List.map (fun (_,seq,_,_ ) -> seq) list_id )
+ @ ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id )
+ in
+ intros_using_then first_intros begin fun fresh_first_intros ->
+ Tacticals.New.tclTHENLIST [
+ intro_using_then (Id.of_string "x") (fun freshn -> induct_on (EConstr.mkVar freshn));
+ intro_using_then (Id.of_string "y") (fun freshm -> destruct_on (EConstr.mkVar freshm));
+ intro_using_then (Id.of_string "Z") begin fun freshz ->
+ Tacticals.New.tclTHENLIST [
+ intros;
+ Tacticals.New.tclTRY (
+ Tacticals.New.tclORELSE reflexivity my_discr_tac
+ );
+ simpl_in_hyp (freshz,Locus.InHyp);
+ (*
repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
-*)
- Tacticals.New.tclREPEAT (
- Tacticals.New.tclTHENLIST [
- Simple.apply_in freshz (EConstr.of_constr (andb_prop()));
- Proofview.Goal.enter begin fun gl ->
- let fresht = fresh_id (Id.of_string "Z") gl in
- destruct_on_as (EConstr.mkVar freshz)
- (IntroOrPattern [[CAst.make @@ IntroNaming (IntroIdentifier fresht);
- CAst.make @@ IntroNaming (IntroIdentifier freshz)]])
- end
- ]);
-(*
+ *)
+ Tacticals.New.tclREPEAT (
+ Tacticals.New.tclTHENLIST [
+ Simple.apply_in freshz (EConstr.of_constr (andb_prop()));
+ destruct_on_as (EConstr.mkVar freshz)
+ (IntroOrPattern [[CAst.make @@ IntroNaming (IntroFresh (Id.of_string "Z"));
+ CAst.make @@ IntroNaming (IntroIdentifier freshz)]])
+ ]);
+ (*
Ci a1 ... an = Ci b1 ... bn
replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto
-*)
- Proofview.Goal.enter begin fun gl ->
- let concl = Proofview.Goal.concl gl in
- let sigma = Tacmach.New.project gl in
- match EConstr.kind sigma concl with
- | App (c,ca) -> (
- match EConstr.kind sigma c with
- | Ind (indeq, u) ->
- if GlobRef.equal (GlobRef.IndRef indeq) Coqlib.(lib_ref "core.eq.type")
- then
- Tacticals.New.tclTHEN
- (do_replace_bl bl_scheme_key ind
- (!avoid)
- nparrec (ca.(2))
- (ca.(1)))
- Auto.default_auto
- else
- Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
- | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.")
- )
- | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
- end
+ *)
+ Proofview.Goal.enter begin fun gl ->
+ let concl = Proofview.Goal.concl gl in
+ let sigma = Tacmach.New.project gl in
+ match EConstr.kind sigma concl with
+ | App (c,ca) -> (
+ match EConstr.kind sigma c with
+ | Ind (indeq, u) ->
+ if GlobRef.equal (GlobRef.IndRef indeq) Coqlib.(lib_ref "core.eq.type")
+ then
+ Tacticals.New.tclTHEN
+ (do_replace_bl bl_scheme_key ind
+ (List.rev fresh_first_intros)
+ nparrec (ca.(2))
+ (ca.(1)))
+ Auto.default_auto
+ else
+ Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
+ | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.")
+ )
+ | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
+ end
- ]
- end
+ ]
+ end
+ ]
+ end
let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
@@ -729,11 +721,11 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
let compute_lb_goal ind lnamesparrec nparrec =
let list_id = list_id lnamesparrec in
let eq = eq () and tt = tt () and bb = bb () in
- let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
- let eqI = eqI ind lnamesparrec in
+ let avoid = avoid_of_list_id list_id in
+ let eqI = eqI ind list_id in
+ let x = next_ident_away (Id.of_string "x") avoid in
+ let y = next_ident_away (Id.of_string "y") (Id.Set.add x avoid) in
let create_input c =
- let x = next_ident_away (Id.of_string "x") avoid and
- y = next_ident_away (Id.of_string "y") avoid in
let lb_typ = List.map (fun (s,seq,_,_) ->
mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) (
mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) (
@@ -760,73 +752,62 @@ let compute_lb_goal ind lnamesparrec nparrec =
in
mkNamedProd x (RelDecl.get_type decl) a) eq_input lnamesparrec
in
- let n = next_ident_away (Id.of_string "x") avoid and
- m = next_ident_away (Id.of_string "y") avoid in
let u = Univ.Instance.empty in
create_input (
- mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd (ind,u) nparrec) (
- mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) (
+ mkNamedProd (make_annot x Sorts.Relevant) (mkFullInd (ind,u) nparrec) (
+ mkNamedProd (make_annot y Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) (
mkArrow
- (mkApp(eq,[|mkFullInd (ind,u) (nparrec+2);mkVar n;mkVar m|]))
+ (mkApp(eq,[|mkFullInd (ind,u) (nparrec+2);mkVar x;mkVar y|]))
Sorts.Relevant
- (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
+ (mkApp(eq,[|bb;mkApp(eqI,[|mkVar x;mkVar y|]);tt|]))
)))
let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
let list_id = list_id lnamesparrec in
- let avoid = ref [] in
- let first_intros =
- ( List.map (fun (s,_,_,_) -> s ) list_id ) @
- ( List.map (fun (_,seq,_,_) -> seq) list_id ) @
- ( List.map (fun (_,_,_,slb) -> slb) list_id )
- in
- let fresh_id s gl =
- let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in
- avoid := fresh::(!avoid); fresh
- in
- Proofview.Goal.enter begin fun gl ->
- let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
- let freshn = fresh_id (Id.of_string "x") gl in
- let freshm = fresh_id (Id.of_string "y") gl in
- let freshz = fresh_id (Id.of_string "Z") gl in
- (* try with *)
- Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros;
- intro_using freshn ;
- induct_on (EConstr.mkVar freshn);
- intro_using freshm;
- destruct_on (EConstr.mkVar freshm);
- intro_using freshz;
- intros;
- Tacticals.New.tclTRY (
- Tacticals.New.tclORELSE reflexivity my_discr_tac
- );
- my_inj_tac freshz;
- intros; simpl_in_concl;
- Auto.default_auto;
- Tacticals.New.tclREPEAT (
- Tacticals.New.tclTHENLIST [apply (EConstr.of_constr (andb_true_intro()));
- simplest_split ;Auto.default_auto ]
- );
- Proofview.Goal.enter begin fun gls ->
- let concl = Proofview.Goal.concl gls in
- let sigma = Tacmach.New.project gl in
- (* assume the goal to be eq (eq_type ...) = true *)
- match EConstr.kind sigma concl with
- | App(c,ca) -> (match (EConstr.kind sigma ca.(1)) with
- | App(c',ca') ->
- let n = Array.length ca' in
- do_replace_lb mode lb_scheme_key
- (!avoid)
- nparrec
- ca'.(n-2) ca'.(n-1)
- | _ ->
- Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
- )
- | _ ->
- Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
- end
- ]
- end
+ let first_intros =
+ ( List.map (fun (s,_,_,_) -> s ) list_id )
+ @ ( List.map (fun (_,seq,_,_) -> seq) list_id )
+ @ ( List.map (fun (_,_,_,slb) -> slb) list_id )
+ in
+ intros_using_then first_intros begin fun fresh_first_intros ->
+ Tacticals.New.tclTHENLIST [
+ intro_using_then (Id.of_string "x") (fun freshn -> induct_on (EConstr.mkVar freshn));
+ intro_using_then (Id.of_string "y") (fun freshm -> destruct_on (EConstr.mkVar freshm));
+ intro_using_then (Id.of_string "Z") begin fun freshz ->
+ Tacticals.New.tclTHENLIST [
+ intros;
+ Tacticals.New.tclTRY (
+ Tacticals.New.tclORELSE reflexivity my_discr_tac
+ );
+ my_inj_tac freshz;
+ intros; simpl_in_concl;
+ Auto.default_auto;
+ Tacticals.New.tclREPEAT (
+ Tacticals.New.tclTHENLIST [apply (EConstr.of_constr (andb_true_intro()));
+ simplest_split ;Auto.default_auto ]
+ );
+ Proofview.Goal.enter begin fun gls ->
+ let concl = Proofview.Goal.concl gls in
+ let sigma = Tacmach.New.project gls in
+ (* assume the goal to be eq (eq_type ...) = true *)
+ match EConstr.kind sigma concl with
+ | App(c,ca) -> (match (EConstr.kind sigma ca.(1)) with
+ | App(c',ca') ->
+ let n = Array.length ca' in
+ do_replace_lb mode lb_scheme_key
+ (List.rev fresh_first_intros)
+ nparrec
+ ca'.(n-2) ca'.(n-1)
+ | _ ->
+ Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
+ )
+ | _ ->
+ Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
+ end
+ ]
+ end
+ ]
+ end
let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
@@ -868,10 +849,10 @@ let compute_dec_goal ind lnamesparrec nparrec =
check_not_is_defined ();
let eq = eq () and tt = tt () and bb = bb () in
let list_id = list_id lnamesparrec in
- let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
+ let avoid = avoid_of_list_id list_id in
+ let x = next_ident_away (Id.of_string "x") avoid in
+ let y = next_ident_away (Id.of_string "y") (Id.Set.add x avoid) in
let create_input c =
- let x = next_ident_away (Id.of_string "x") avoid and
- y = next_ident_away (Id.of_string "y") avoid in
let lb_typ = List.map (fun (s,seq,_,_) ->
mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) (
mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) (
@@ -912,12 +893,10 @@ let compute_dec_goal ind lnamesparrec nparrec =
in
mkNamedProd x (RelDecl.get_type decl) a) eq_input lnamesparrec
in
- let n = next_ident_away (Id.of_string "x") avoid and
- m = next_ident_away (Id.of_string "y") avoid in
- let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar n;mkVar m|]) in
+ let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar x;mkVar y|]) in
create_input (
- mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd ind (2*nparrec)) (
- mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd ind (2*nparrec+1)) (
+ mkNamedProd (make_annot x Sorts.Relevant) (mkFullInd ind (2*nparrec)) (
+ mkNamedProd (make_annot y Sorts.Relevant) (mkFullInd ind (2*nparrec+1)) (
mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|])
)
)
@@ -925,83 +904,89 @@ let compute_dec_goal ind lnamesparrec nparrec =
let compute_dec_tact ind lnamesparrec nparrec =
let eq = eq () and tt = tt ()
- and ff = ff () and bb = bb () in
+ and ff = ff () and bb = bb () in
let list_id = list_id lnamesparrec in
find_scheme beq_scheme_kind ind >>= fun _ ->
- let eqI = eqI ind lnamesparrec in
- let avoid = ref [] in
+ let _non_fresh_eqI = eqI ind list_id in
let eqtrue x = mkApp(eq,[|bb;x;tt|]) in
let eqfalse x = mkApp(eq,[|bb;x;ff|]) in
let first_intros =
- ( List.map (fun (s,_,_,_) -> s ) list_id ) @
- ( List.map (fun (_,seq,_,_) -> seq) list_id ) @
- ( List.map (fun (_,_,sbl,_) -> sbl) list_id ) @
- ( List.map (fun (_,_,_,slb) -> slb) list_id )
- in
- let fresh_id s gl =
- let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in
- avoid := fresh::(!avoid); fresh
+ ( List.map (fun (s,_,_,_) -> s ) list_id )
+ @ ( List.map (fun (_,seq,_,_) -> seq) list_id )
+ @ ( List.map (fun (_,_,sbl,_) -> sbl) list_id )
+ @ ( List.map (fun (_,_,_,slb) -> slb) list_id )
in
- Proofview.Goal.enter begin fun gl ->
- let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
- let freshn = fresh_id (Id.of_string "x") gl in
- let freshm = fresh_id (Id.of_string "y") gl in
- let freshH = fresh_id (Id.of_string "H") gl in
- let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in
- let arfresh = Array.of_list fresh_first_intros in
- let xargs = Array.sub arfresh 0 (2*nparrec) in
- find_scheme bl_scheme_kind ind >>= fun c ->
- let blI = mkConst c in
- find_scheme lb_scheme_kind ind >>= fun c ->
- let lbI = mkConst c in
- Tacticals.New.tclTHENLIST [
- intros_using fresh_first_intros;
- intros_using [freshn;freshm];
- (*we do this so we don't have to prove the same goal twice *)
- assert_by (Name freshH) (EConstr.of_constr (
- mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
- ))
- (Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto);
-
+ let fresh_id s gl = fresh_id_in_env (Id.Set.empty) s (Proofview.Goal.env gl) in
+ intros_using_then first_intros begin fun fresh_first_intros ->
+ let eqI =
+ let a = Array.of_list fresh_first_intros in
+ let n = List.length list_id in
+ assert (Int.equal (Array.length a) (4 * n));
+ let fresh_list_id =
+ List.init n (fun i -> (Array.get a i, Array.get a (i+n),
+ Array.get a (i+2*n), Array.get a (i+3*n))) in
+ eqI ind fresh_list_id
+ in
+ intro_using_then (Id.of_string "x") begin fun freshn ->
+ intro_using_then (Id.of_string "y") begin fun freshm ->
Proofview.Goal.enter begin fun gl ->
- let freshH2 = fresh_id (Id.of_string "H") gl in
- Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [
- (* left *)
- Tacticals.New.tclTHENLIST [
- simplest_left;
- apply (EConstr.of_constr (mkApp(blI,Array.map mkVar xargs)));
- Auto.default_auto
- ]
- ;
-
- (*right *)
- Proofview.Goal.enter begin fun gl ->
- let freshH3 = fresh_id (Id.of_string "H") gl in
- Tacticals.New.tclTHENLIST [
- simplest_right ;
- unfold_constr (Coqlib.lib_ref "core.not.type");
- intro;
- Equality.subst_all ();
- assert_by (Name freshH3)
- (EConstr.of_constr (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|])))
- (Tacticals.New.tclTHENLIST [
- apply (EConstr.of_constr (mkApp(lbI,Array.map mkVar xargs)));
- Auto.default_auto
- ]);
- Equality.general_rewrite_bindings_in true
- Locus.AllOccurrences true false
- (List.hd !avoid)
- ((EConstr.mkVar (List.hd (List.tl !avoid))),
- NoBindings
- )
- true;
- my_discr_tac
+ let freshH = fresh_id (Id.of_string "H") gl in
+ let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in
+ let arfresh = Array.of_list fresh_first_intros in
+ let xargs = Array.sub arfresh 0 (2*nparrec) in
+ find_scheme bl_scheme_kind ind >>= fun c ->
+ let blI = mkConst c in
+ find_scheme lb_scheme_kind ind >>= fun c ->
+ let lbI = mkConst c in
+ Tacticals.New.tclTHENLIST [
+ (*we do this so we don't have to prove the same goal twice *)
+ assert_by (Name freshH) (EConstr.of_constr (
+ mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
+ ))
+ (Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto);
+
+ Proofview.Goal.enter begin fun gl ->
+ let freshH2 = fresh_id (Id.of_string "H") gl in
+ Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [
+ (* left *)
+ Tacticals.New.tclTHENLIST [
+ simplest_left;
+ apply (EConstr.of_constr (mkApp(blI,Array.map mkVar xargs)));
+ Auto.default_auto
+ ]
+ ;
+
+ (*right *)
+ Proofview.Goal.enter begin fun gl ->
+ let freshH3 = fresh_id (Id.of_string "H") gl in
+ Tacticals.New.tclTHENLIST [
+ simplest_right ;
+ unfold_constr (Coqlib.lib_ref "core.not.type");
+ intro;
+ Equality.subst_all ();
+ assert_by (Name freshH3)
+ (EConstr.of_constr (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|])))
+ (Tacticals.New.tclTHENLIST [
+ apply (EConstr.of_constr (mkApp(lbI,Array.map mkVar xargs)));
+ Auto.default_auto
+ ]);
+ Equality.general_rewrite_bindings_in true
+ Locus.AllOccurrences true false
+ freshH3
+ ((EConstr.mkVar freshH2),
+ NoBindings
+ )
+ true;
+ my_discr_tac
+ ]
+ end
+ ]
+ end
]
- end
- ]
+ end
end
- ]
- end
+ end
+ end
let make_eq_decidability mode mind =
let mib = Global.lookup_mind mind in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index f454c389dc..02cb60f1cf 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -358,8 +358,9 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id
the pretyping after the proof has opened. As a
consequence, we use the low-level primitives to code
the refinement manually.*)
- let gls = List.rev (Evd.future_goals sigma) in
- let sigma = Evd.reset_future_goals sigma in
+ let future_goals, sigma = Evd.pop_future_goals sigma in
+ let gls = List.rev future_goals.Evd.FutureGoals.comb in
+ let sigma = Evd.push_future_goals sigma in
let kind = Decls.(IsDefinition Instance) in
let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in
let info = Declare.Info.make ~hook ~kind ~udecl ~poly () in
diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml
index 360e228bfc..adf1f42beb 100644
--- a/vernac/comArguments.ml
+++ b/vernac/comArguments.ml
@@ -213,22 +213,13 @@ let vernac_arguments ~section_local reference args more_implicits flags =
in CErrors.user_err ~hdr:"vernac_declare_arguments" msg
end;
- let duplicate_names =
- List.duplicates Name.equal (List.filter ((!=) Anonymous) names)
- in
- if not (List.is_empty duplicate_names) then begin
- CErrors.user_err Pp.(strbrk "Some argument names are duplicated: " ++
- prlist_with_sep pr_comma Name.print duplicate_names)
- end;
-
let implicits =
List.map (fun { name; implicit_status = i } -> (name,i)) args
in
let implicits = implicits :: more_implicits in
- let implicits = List.map (List.map snd) implicits in
let implicits_specified = match implicits with
- | [l] -> List.exists (function Glob_term.Explicit -> false | _ -> true) l
+ | [l] -> List.exists (function _, Glob_term.Explicit -> false | _ -> true) l
| _ -> true in
if implicits_specified && clear_implicits_flag then
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 0f34adf1c7..564d24c1ea 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -247,6 +247,7 @@ let interp_fixpoint ?(check_recursivity=true) ~cofix l :
(EConstr.rel_context * Impargs.manual_implicits * int option) list) =
let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in
if check_recursivity then check_recursive true env evd fix;
+ let evd = Pretyping.(solve_remaining_evars all_no_fail_flags env evd) in
let uctx,fix = ground_fixpoint env evd fix in
(fix,pl,uctx,info)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 673124296d..452de69b1d 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -451,7 +451,7 @@ let interp_params env udecl uparamsl paramsl =
do the unification.
[env_ar_par] is [uparams; inds; params]
*)
-let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams c =
+let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams ~binders:k c =
let is_ind sigma k c = match EConstr.kind sigma c with
| Constr.Rel n ->
(* env is [uparams; inds; params; k other things] *)
@@ -462,14 +462,18 @@ let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams c =
| Constr.App (h,args) when is_ind sigma k h ->
Array.fold_left_i (fun i sigma arg ->
if i >= nparams || not (EConstr.isEvar sigma arg) then sigma
- else Evarconv.unify_delay env sigma arg (EConstr.mkRel (k+nparams-i)))
+ else begin try Evarconv.unify_delay env sigma arg (EConstr.mkRel (k+nparams-i))
+ with Evarconv.UnableToUnify _ ->
+ (* ignore errors, we will get a "Cannot infer ..." error instead *)
+ sigma
+ end)
sigma args
| _ -> Termops.fold_constr_with_full_binders
sigma
(fun d (env,k) -> EConstr.push_rel d env, k+1)
aux envk sigma c
in
- aux (env_ar_par,0) sigma c
+ aux (env_ar_par,k) sigma c
let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite =
check_all_names_different indl;
@@ -527,7 +531,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let sigma =
List.fold_left (fun sigma (_,ctyps,_) ->
List.fold_left (fun sigma ctyp ->
- maybe_unify_params_in env_ar_params sigma ~ninds ~nparams ctyp)
+ maybe_unify_params_in env_ar_params sigma ~ninds ~nparams ~binders:0 ctyp)
sigma ctyps)
sigma constructors
in
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 9c876787a3..91e8f609d5 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -81,8 +81,8 @@ val template_polymorphism_candidate
monomorphic universe context that can be made parametric in its
conclusion sort, if one is given. *)
-val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int
+val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int -> binders:int
-> EConstr.t -> Evd.evar_map
(** [nparams] is the number of parameters which aren't treated as
uniform, ie the length of params (including letins) where the env
- is [uniform params, inductives, params]. *)
+ is [uniform params, inductives, params, binders]. *)
diff --git a/vernac/declare.ml b/vernac/declare.ml
index eedbee852b..099a63cf8f 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -642,14 +642,32 @@ let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe =
dref
(* Preparing proof entries *)
+let error_unresolved_evars env sigma t evars =
+ let pr_unresolved_evar e =
+ hov 2 (str"- " ++ Printer.pr_existential_key sigma e ++ str ": " ++
+ Himsg.explain_pretype_error env sigma
+ (Pretype_errors.UnsolvableImplicit (e,None)))
+ in
+ CErrors.user_err (hov 0 begin
+ str "The following term contains unresolved implicit arguments:"++ fnl () ++
+ str " " ++ Printer.pr_econstr_env env sigma t ++ fnl () ++
+ str "More precisely: " ++ fnl () ++
+ v 0 (prlist_with_sep cut pr_unresolved_evar (Evar.Set.elements evars))
+ end)
+
+let check_evars_are_solved env sigma t =
+ let t = EConstr.of_constr t in
+ let evars = Evarutil.undefined_evars_of_term sigma t in
+ if not (Evar.Set.is_empty evars) then error_unresolved_evars env sigma t evars
let prepare_definition ~info ~opaque ~body ~typ sigma =
let { Info.poly; udecl; inline; _ } = info in
let env = Global.env () in
- Pretyping.check_evars_are_solved ~program_mode:false env sigma;
- let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true
+ let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
sigma (fun nf -> nf body, Option.map nf typ)
in
+ Option.iter (check_evars_are_solved env sigma) types;
+ check_evars_are_solved env sigma body;
let univs = Evd.check_univ_decl ~poly sigma udecl in
let entry = definition_entry ~opaque ~inline ?types ~univs body in
let uctx = Evd.evar_universe_context sigma in
@@ -1535,11 +1553,11 @@ let set_used_variables ps l =
ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) }
let get_open_goals ps =
- let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
+ let Proof.{ goals; stack; sigma } = Proof.data ps.proof in
List.length goals +
List.fold_left (+) 0
(List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
- List.length shelf
+ List.length (Evd.shelf sigma)
type proof_object =
{ name : Names.Id.t
@@ -1716,12 +1734,8 @@ let return_proof ps =
let p, uctx = prepare_proof ~unsafe_typ:false ps in
List.map (fun (((_ub, body),eff),_) -> (body,eff)) p, uctx
-let update_global_env =
- map ~f:(fun p ->
- let { Proof.sigma } = Proof.data p in
- let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
- let p, (status,info), _ = Proof.run_tactic (Global.env ()) tac p in
- p)
+let update_sigma_univs ugraph p =
+ map ~f:(Proof.update_sigma_univs ugraph) p
let next = let n = ref 0 in fun () -> incr n; !n
@@ -2000,7 +2014,7 @@ let finish_derived ~f ~name ~entries =
let lemma_def = Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in
let lemma_def = DefinitionEntry lemma_def in
let ct = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in
- [GlobRef.ConstRef ct]
+ [GlobRef.ConstRef f_kn; GlobRef.ConstRef ct]
let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 =
@@ -2237,7 +2251,7 @@ let rec solve_obligation prg num tac =
let scope = Locality.Global Locality.ImportNeedQualified in
let kind = kind_of_obligation (snd obl.obl_status) in
let evd = Evd.from_ctx (Internal.get_uctx prg) in
- let evd = Evd.update_sigma_env evd (Global.env ()) in
+ let evd = Evd.update_sigma_univs (Global.universes ()) evd in
let auto ~pm n oblset tac = auto_solve_obligations ~pm n ~oblset tac in
let proof_ending =
let name = Internal.get_name prg in
@@ -2278,7 +2292,7 @@ and solve_obligation_by_tac prg obls i tac =
| None -> !default_tactic
in
let uctx = Internal.get_uctx prg in
- let uctx = UState.update_sigma_env uctx (Global.env ()) in
+ let uctx = UState.update_sigma_univs uctx (Global.universes ()) in
let poly = Internal.get_poly prg in
match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac ~poly ~uctx with
| None -> None
diff --git a/vernac/declare.mli b/vernac/declare.mli
index c5a8afbad5..1ad79928d5 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -117,8 +117,7 @@ end
normalized w.r.t. the passed [evar_map] [sigma]. Universes should
be handled properly, including minimization and restriction. Note
that [sigma] is checked for unresolved evars, thus you should be
- careful not to submit open terms or evar maps with stale,
- unresolved existentials *)
+ careful not to submit open terms *)
val declare_definition
: info:Info.t
-> cinfo:EConstr.t option CInfo.t
@@ -247,10 +246,10 @@ module Proof : sig
val compact : t -> t
- (** Update the proofs global environment after a side-effecting command
- (e.g. a sublemma definition) has been run inside it. Assumes
- there_are_pending_proofs. *)
- val update_global_env : t -> t
+ (** Update the proof's universe information typically after a
+ side-effecting command (e.g. a sublemma definition) has been run
+ inside it. *)
+ val update_sigma_univs : UGraph.t -> t -> t
val get_open_goals : t -> int
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 6cc48d0e48..0bdcd53c92 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -665,15 +665,21 @@ let expand_list_rule s typ tkl x n p ll =
aux (i+1) (main :: tks @ hds) ll in
aux 0 [] ll
-let is_constr_typ typ x etyps =
+let is_constr_typ (s,lev) x etyps =
match List.assoc x etyps with
- | ETConstr (_,_,typ') -> typ = typ'
+ (* TODO: factorize these rules with the ones computing the effective
+ sublevel sent to camlp5, so as to include the case of
+ DefaultLevel which are valid *)
+ | ETConstr (s',_,(lev',InternalProd | (NumLevel _ | NextLevel as lev'), _)) ->
+ Notation.notation_entry_eq s s' && production_level_eq lev lev'
| _ -> false
let include_possible_similar_trailing_pattern typ etyps sl l =
let rec aux n = function
| Terminal s :: sl, Terminal s'::l' when s = s' -> aux n (sl,l')
| [], NonTerminal x ::l' when is_constr_typ typ x etyps -> try_aux n l'
+ | Break _ :: sl, l -> aux n (sl,l)
+ | sl, Break _ :: l -> aux n (sl,l)
| _ -> raise Exit
and try_aux n l =
try aux (n+1) (sl,l)
@@ -704,8 +710,8 @@ let make_production etyps symbols =
| Break _ -> []
| _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator.")) sl) in
match List.assoc x etyps with
- | ETConstr (s,_,typ) ->
- let p,l' = include_possible_similar_trailing_pattern typ etyps sl l in
+ | ETConstr (s,_,(lev,_ as typ)) ->
+ let p,l' = include_possible_similar_trailing_pattern (s,lev) etyps sl l in
expand_list_rule s typ tkl x 1 p (aux l')
| ETBinder o ->
check_open_binder o sl x;
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 2b46542287..8b00484b4a 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -75,12 +75,12 @@ let print_ref reduce ref udecl =
let inst = Univ.make_abstract_instance univs in
let bl = Printer.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in
let sigma = Evd.from_ctx (UState.of_binders bl) in
- let typ = EConstr.of_constr typ in
let typ =
if reduce then
- let ctx,ccl = Reductionops.splay_prod_assum env sigma typ
- in EConstr.it_mkProd_or_LetIn ccl ctx
+ let ctx,ccl = Reductionops.splay_prod_assum env sigma (EConstr.of_constr typ)
+ in EConstr.to_constr sigma (EConstr.it_mkProd_or_LetIn ccl ctx)
else typ in
+ let typ = Arguments_renaming.rename_type typ ref in
let impargs = select_stronger_impargs (implicits_of_global ref) in
let impargs = List.map binding_kind_of_status impargs in
let variance = let open GlobRef in match ref with
@@ -95,7 +95,7 @@ let print_ref reduce ref udecl =
else mt ()
in
let priv = None in (* We deliberately don't print private univs in About. *)
- hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma ~impargs typ ++
+ hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma ~impargs typ ++
Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv)
(********************************)
@@ -261,6 +261,10 @@ let implicit_kind_of_status = function
| None -> Anonymous, Glob_term.Explicit
| Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit
+let extra_implicit_kind_of_status imp =
+ let _,imp = implicit_kind_of_status imp in
+ (Anonymous, imp)
+
let dummy = {
Vernacexpr.implicit_status = Glob_term.Explicit;
name = Anonymous;
@@ -268,8 +272,10 @@ let dummy = {
notation_scope = None;
}
-let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} =
- name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit
+let is_dummy = function
+ | Vernacexpr.(RealArg {implicit_status; name; recarg_like; notation_scope}) ->
+ name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit
+ | _ -> false
let rec main_implicits i renames recargs scopes impls =
if renames = [] && recargs = [] && scopes = [] && impls = [] then []
@@ -292,9 +298,7 @@ let rec main_implicits i renames recargs scopes impls =
let tl = function [] -> [] | _::tl -> tl in
(* recargs is special -> tl handled above *)
let rest = main_implicits (i+1) (tl renames) recargs (tl scopes) (tl impls) in
- if is_dummy status && rest = []
- then [] (* we may have a trail of dummies due to eg "clear scopes" *)
- else status :: rest
+ status :: rest
let rec insert_fake_args volatile bidi impls =
let open Vernacexpr in
@@ -320,11 +324,7 @@ let print_arguments ref =
| Some (UnfoldWhen { nargs; recargs }) -> [], recargs, nargs
| Some (UnfoldWhenNoMatch { nargs; recargs }) -> [`ReductionDontExposeCase], recargs, nargs
in
- let flags, renames = match Arguments_renaming.arguments_names ref with
- | exception Not_found -> flags, []
- | [] -> flags, []
- | renames -> `Rename::flags, renames
- in
+ let renames = try Arguments_renaming.arguments_names ref with Not_found -> [] in
let scopes = Notation.find_arguments_scope ref in
let flags = if needs_extra_scopes ref scopes then `ExtraScopes::flags else flags in
let impls = Impargs.extract_impargs_data (Impargs.implicits_of_global ref) in
@@ -333,15 +333,17 @@ let print_arguments ref =
| [] -> assert false
in
let impls = main_implicits 0 renames recargs scopes impls in
- let moreimpls = List.map (fun (_,i) -> List.map implicit_kind_of_status i) moreimpls in
+ let moreimpls = List.map (fun (_,i) -> List.map extra_implicit_kind_of_status i) moreimpls in
let bidi = Pretyping.get_bidirectionality_hint ref in
let impls = insert_fake_args nargs_for_red bidi impls in
- if impls = [] && moreimpls = [] && flags = [] then []
+ if List.for_all is_dummy impls && moreimpls = [] && flags = [] then []
else
let open Constrexpr in
let open Vernacexpr in
[Ppvernac.pr_vernac_expr
- (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags))]
+ (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags)) ++
+ (if renames = [] then mt () else
+ fnl () ++ str " (where some original arguments have been renamed)")]
let print_name_infos ref =
let type_info_for_implicit =
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 2130a398e9..95680c2a4e 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -41,28 +41,27 @@ let set_of_type env ty =
let full_set env =
List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
-let rec process_expr env e ty =
+let process_expr env e v_ty =
let rec aux = function
| SsEmpty -> Id.Set.empty
- | SsType -> set_of_type env ty
- | SsSingl { CAst.v = id } -> set_of_id env id
+ | SsType -> v_ty
+ | SsSingl { CAst.v = id } -> set_of_id id
| SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
| SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
| SsCompl e -> Id.Set.diff (full_set env) (aux e)
| SsFwdClose e -> close_fwd env (aux e)
+ and set_of_id id =
+ if Id.to_string id = "All" then
+ full_set env
+ else if CList.mem_assoc_f Id.equal id !known_names then
+ aux (CList.assoc_f Id.equal id !known_names)
+ else Id.Set.singleton id
in
- aux e
-
-and set_of_id env id =
- if Id.to_string id = "All" then
- List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
- else if CList.mem_assoc_f Id.equal id !known_names then
- process_expr env (CList.assoc_f Id.equal id !known_names) []
- else Id.Set.singleton id
+ aux e
let process_expr env e ty =
let v_ty = set_of_type env ty in
- let s = Id.Set.union v_ty (process_expr env e ty) in
+ let s = Id.Set.union v_ty (process_expr env e v_ty) in
Id.Set.elements s
let name_set id expr = known_names := (id,expr) :: !known_names
diff --git a/vernac/record.ml b/vernac/record.ml
index d0036e40f9..bd5b71cd6b 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -81,12 +81,12 @@ let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l =
(EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls))
(env, sigma, [], [], impls_env) nots l
in
- let _, sigma = Context.Rel.fold_outside ~init:(env,sigma) (fun f (env,sigma) ->
+ let _, _, sigma = Context.Rel.fold_outside ~init:(env,0,sigma) (fun f (env,k,sigma) ->
let sigma = RelDecl.fold_constr (fun c sigma ->
- ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams c)
+ ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams ~binders:k c)
f sigma
in
- EConstr.push_rel f env, sigma)
+ EConstr.push_rel f env, k+1, sigma)
newfs
in
sigma, (impls, newfs)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d540e7f93d..6a4c2a626d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -112,7 +112,9 @@ let show_proof ~pstate =
let show_top_evars ~proof =
(* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
- let Proof.{goals;shelf;given_up;sigma} = Proof.data proof in
+ let Proof.{goals; sigma} = Proof.data proof in
+ let shelf = Evd.shelf sigma in
+ let given_up = Evar.Set.elements @@ Evd.given_up sigma in
pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma)
let show_universes ~proof =
@@ -345,17 +347,21 @@ let dump_universes_gen prl g s =
close ();
Exninfo.iraise reraise
-let universe_subgraph ?loc g univ =
+let universe_subgraph ?loc kept univ =
let open Univ in
let sigma = Evd.from_env (Global.env()) in
- let univs_of q =
+ let parse q =
let q = Glob_term.(GType q) in
(* this function has a nice error message for not found univs *)
- LSet.singleton (Pretyping.interp_known_glob_level ?loc sigma q)
+ Pretyping.interp_known_glob_level ?loc sigma q
in
- let univs = List.fold_left (fun univs q -> LSet.union univs (univs_of q)) LSet.empty g in
- let csts = UGraph.constraints_for ~kept:(LSet.add Level.prop (LSet.add Level.set univs)) univ in
- let univ = LSet.fold UGraph.add_universe_unconstrained univs UGraph.initial_universes in
+ let kept = List.fold_left (fun kept q -> LSet.add (parse q) kept) LSet.empty kept in
+ let csts = UGraph.constraints_for ~kept univ in
+ let add u newgraph =
+ let strict = UGraph.check_constraint univ (Level.set,Lt,u) in
+ UGraph.add_universe u ~lbound:UGraph.Bound.Set ~strict newgraph
+ in
+ let univ = LSet.fold add kept UGraph.initial_universes in
UGraph.merge_constraints csts univ
let print_universes ?loc ~sort ~subgraph dst =
@@ -1511,15 +1517,15 @@ let () =
declare_bool_option
{ optdepr = false;
optkey = ["Dump";"Bytecode"];
- optread = (fun () -> !Cbytegen.dump_bytecode);
- optwrite = (:=) Cbytegen.dump_bytecode }
+ optread = (fun () -> !Vmbytegen.dump_bytecode);
+ optwrite = (:=) Vmbytegen.dump_bytecode }
let () =
declare_bool_option
{ optdepr = false;
optkey = ["Dump";"Lambda"];
- optread = (fun () -> !Clambda.dump_lambda);
- optwrite = (:=) Clambda.dump_lambda }
+ optread = (fun () -> !Vmlambda.dump_lambda);
+ optwrite = (:=) Vmlambda.dump_lambda }
let () =
declare_bool_option
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 6be2fb0d43..edf48fef1a 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -211,8 +211,11 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) =
(fun ~st ->
let before_univs = Global.universes () in
let pstack, pm = interp_expr ~atts:cmd.attrs ~st cmd.expr in
- if before_univs == Global.universes () then pstack, pm
- else Option.map (Vernacstate.LemmaStack.map_top ~f:Declare.Proof.update_global_env) pstack, pm)
+ let after_univs = Global.universes () in
+ if before_univs == after_univs then pstack, pm
+ else
+ let f = Declare.Proof.update_sigma_univs after_univs in
+ Option.map (Vernacstate.LemmaStack.map ~f) pstack, pm)
~st
(* XXX: This won't properly set the proof mode, as of today, it is
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index ee06205427..204008997d 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -80,7 +80,7 @@ module LemmaStack = struct
type t = Declare.Proof.t * Declare.Proof.t list
- let map f (pf, pfl) = (f pf, List.map f pfl)
+ let map ~f (pf, pfl) = (f pf, List.map f pfl)
let map_top ~f (pf, pfl) = (f pf, pfl)
let pop (ps, p) = match p with
@@ -96,7 +96,7 @@ module LemmaStack = struct
let get_all_proof_names (pf : t) =
let prj x = Declare.Proof.get x in
- let (pn, pns) = map Proof.(function pf -> (data (prj pf)).name) pf in
+ let (pn, pns) = map ~f:Proof.(function pf -> (data (prj pf)).name) pf in
pn :: pns
let copy_info src tgt =
@@ -218,7 +218,7 @@ module Declare_ = struct
Declare.Proof.info pt)
let discard_all () = s_lemmas := None
- let update_global_env () = dd (Declare.Proof.update_global_env)
+ let update_sigma_univs ugraph = dd (Declare.Proof.update_sigma_univs ugraph)
let get_current_context () = cc Declare.Proof.get_current_context
@@ -267,6 +267,7 @@ module Stm = struct
end
}
+ type non_pstate = Summary.frozen * Lib.frozen
let non_pstate { system } =
let st = System.Stm.summary system in
let st = Summary.remove_from_summary st Evarutil.meta_counter_summary_tag in
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 16fab3782b..e1b13dcb73 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -40,6 +40,7 @@ module LemmaStack : sig
val pop : t -> Declare.Proof.t * t option
val push : t option -> Declare.Proof.t -> t
+ val map : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t
val map_top : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t
val with_top : t -> f:(Declare.Proof.t -> 'a ) -> 'a
@@ -64,15 +65,23 @@ val unfreeze_interp_state : t -> unit
(* WARNING: Do not use, it will go away in future releases *)
val invalidate_cache : unit -> unit
-(* STM-specific state handling *)
+(** STM-specific state handling *)
module Stm : sig
+
+ (** Proof state + meta/evar counters *)
type pstate
- (** Surgery on states related to proof state *)
val pstate : t -> pstate
val set_pstate : t -> pstate -> t
- val non_pstate : t -> Summary.frozen * Lib.frozen
+
+ (** Rest of the state, unfortunately this is used in low-level so we need to expose it *)
+ type non_pstate = Summary.frozen * Lib.frozen
+ val non_pstate : t -> non_pstate
+
+ (** Checks if two states have the same Environ.env (physical eq) *)
val same_env : t -> t -> bool
+
+ (** Call [Lib.drop_objects] on the state *)
val make_shallow : t -> t
end
@@ -104,7 +113,7 @@ module Declare : sig
val close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof
val discard_all : unit -> unit
- val update_global_env : unit -> unit
+ val update_sigma_univs : UGraph.t -> unit
val get_current_context : unit -> Evd.evar_map * Environ.env
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 06:57:21 +0000