aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml30
-rw-r--r--proofs/clenv.mli6
-rw-r--r--proofs/clenvtac.ml8
-rw-r--r--proofs/logic.ml68
-rw-r--r--proofs/pfedit.ml19
-rw-r--r--proofs/pfedit.mli15
-rw-r--r--proofs/proof.mli3
-rw-r--r--proofs/proof_global.ml41
-rw-r--r--proofs/proof_global.mli7
-rw-r--r--proofs/proofview.ml9
-rw-r--r--proofs/proofview.mli2
-rw-r--r--proofs/refiner.ml17
-rw-r--r--proofs/refiner.mli6
-rw-r--r--proofs/tacmach.ml6
-rw-r--r--proofs/tacmach.mli7
15 files changed, 172 insertions, 72 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 64a9f00245..afc8d3b70d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -42,12 +42,27 @@ type clausenv = {
let cl_env ce = ce.env
let cl_sigma ce = ce.evd
+let map_clenv sub clenv =
+ { templval = map_fl sub clenv.templval;
+ templtyp = map_fl sub clenv.templtyp;
+ evd = cmap sub clenv.evd;
+ env = clenv.env }
+
let clenv_nf_meta clenv c = nf_meta clenv.evd c
let clenv_term clenv c = meta_instance clenv.evd c
let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
let clenv_value clenv = meta_instance clenv.evd clenv.templval
let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
+let refresh_undefined_univs clenv =
+ match kind_of_term clenv.templval.rebus with
+ | Var _ -> clenv, Univ.empty_level_subst
+ | App (f, args) when isVar f -> clenv, Univ.empty_level_subst
+ | _ ->
+ let evd', subst = Evd.refresh_undefined_universes clenv.evd in
+ let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in
+ { clenv with evd = evd'; templval = map_freelisted clenv.templval;
+ templtyp = map_freelisted clenv.templtyp }, subst
let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
@@ -239,14 +254,14 @@ let clenv_dependent ce = clenv_dependent_gen false ce
(******************************************************************)
-let clenv_unify ?(flags=default_unify_flags) cv_pb t1 t2 clenv =
+let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
{ clenv with
evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 }
-let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
+let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
{ clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
-let clenv_unique_resolver ?(flags=default_unify_flags) clenv gl =
+let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
let concl = Goal.V82.concl clenv.evd (sig_it gl) in
if isMeta (fst (decompose_appvect (whd_nored clenv.evd clenv.templtyp.rebus))) then
clenv_unify CUMUL ~flags (clenv_type clenv) concl
@@ -305,6 +320,9 @@ let connect_clenv gls clenv =
evd = evd ;
env = Goal.V82.env evd (sig_it gls) }
+(* let connect_clenv_key = Profile.declare_profile "connect_clenv";; *)
+(* let connect_clenv = Profile.profile2 connect_clenv_key connect_clenv *)
+
(* [clenv_fchain mv clenv clenv']
*
* Resolves the value of "mv" (which must be undefined) in clenv to be
@@ -329,11 +347,11 @@ let connect_clenv gls clenv =
In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma].
*)
-let fchain_flags =
- { default_unify_flags with
+let fchain_flags () =
+ { (default_unify_flags ()) with
allow_K_in_toplevel_higher_order_unification = true }
-let clenv_fchain ?(flags=fchain_flags) mv clenv nextclenv =
+let clenv_fchain ?(flags=fchain_flags ()) mv clenv nextclenv =
(* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
let clenv' =
{ templval = clenv.templval;
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index ab4f3af795..35bed8f403 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -23,6 +23,9 @@ type clausenv = {
out *)
templtyp : constr freelisted (** its type *)}
+
+val map_clenv : (constr -> constr) -> clausenv -> clausenv
+
(** subject of clenv (instantiated) *)
val clenv_value : clausenv -> constr
@@ -41,6 +44,9 @@ val mk_clenv_from_n :
val mk_clenv_type_of : Goal.goal sigma -> constr -> clausenv
val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
+(** Refresh the universes in a clenv *)
+val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
+
(** {6 linking of clenvs } *)
val connect_clenv : Goal.goal sigma -> clausenv -> clausenv
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 7a1a14bdec..112402bca9 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -29,6 +29,7 @@ let clenv_cast_meta clenv =
match kind_of_term u with
| App _ | Case _ -> crec_hd u
| Cast (c,_,_) when isMeta c -> u
+ | Proj (p, c) -> mkProj (p, crec_hd c)
| _ -> map_constr crec u
and crec_hd u =
@@ -43,6 +44,7 @@ let clenv_cast_meta clenv =
| App(f,args) -> mkApp (crec_hd f, Array.map crec args)
| Case(ci,p,c,br) ->
mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
+ | Proj (p, c) -> mkProj (p, crec_hd c)
| _ -> u
in
crec
@@ -68,15 +70,15 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls =
in
let clenv = { clenv with evd = evd' } in
tclTHEN
- (tclEVARS evd')
- (refine (clenv_cast_meta clenv (clenv_value clenv)))
+ (tclEVARS (Evd.clear_metas evd'))
+ (refine_no_check (clenv_cast_meta clenv (clenv_value clenv)))
gls
open Unification
let dft = default_unify_flags
-let res_pf clenv ?(with_evars=false) ?(flags=dft) gls =
+let res_pf clenv ?(with_evars=false) ?(flags=dft ()) gls =
clenv_refine with_evars (clenv_unique_resolver ~flags clenv gls) gls
(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 054e6db6c1..02f3a16d85 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -324,6 +324,7 @@ let collect_meta_variables c =
| Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
| Cast(c,_,_) -> collrec deep acc c
| (App _| Case _) -> fold_constr (collrec deep) acc c
+ | Proj (_, c) -> collrec deep acc c
| _ -> fold_constr (collrec true) acc c
in
List.rev (collrec false [] c)
@@ -333,12 +334,15 @@ let check_meta_variables c =
raise (RefinerError (NonLinearProof c))
let check_conv_leq_goal env sigma arg ty conclty =
- if !check && not (is_conv_leq env sigma ty conclty) then
- raise (RefinerError (BadType (arg,ty,conclty)))
+ if !check then
+ let evm, b = Reductionops.infer_conv env sigma ty conclty in
+ if b then evm
+ else raise (RefinerError (BadType (arg,ty,conclty)))
+ else sigma
let goal_type_of env sigma c =
if !check then type_of env sigma c
- else Retyping.get_type_of ~refresh:true env sigma c
+ else Retyping.get_type_of env sigma c
let rec mk_refgoals sigma goal goalacc conclty trm =
let env = Goal.V82.env sigma goal in
@@ -346,17 +350,22 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
let mk_goal hyps concl =
Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal)
in
- match kind_of_term trm with
- | Meta _ ->
+ if (not !check) && not (occur_meta trm) then
+ let t'ty = Retyping.get_type_of env sigma trm in
+ let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
+ (goalacc,t'ty,sigma,trm)
+ else
+ match kind_of_term trm with
+ | Meta _ ->
let conclty = nf_betaiota sigma conclty in
if !check && occur_meta conclty then
raise (RefinerError (MetaInType conclty));
let (gl,ev,sigma) = mk_goal hyps conclty in
gl::goalacc, conclty, sigma, ev
- | Cast (t,k, ty) ->
+ | Cast (t,k, ty) ->
check_typability env sigma ty;
- check_conv_leq_goal env sigma trm ty conclty;
+ let sigma = check_conv_leq_goal env sigma trm ty conclty in
let res = mk_refgoals sigma goal goalacc ty t in
(** we keep the casts (in particular VMcast and NATIVEcast) except
when they are annotating metas *)
@@ -368,11 +377,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
let ans = if ans == t then trm else mkCast(ans,k,ty) in
(gls,cty,sigma,ans)
- | App (f,l) ->
+ | App (f,l) ->
let (acc',hdty,sigma,applicand) =
match kind_of_term f with
| Ind _ | Const _
- when (isInd f || has_polymorphic_type (destConst f)) ->
+ when (isInd f || has_polymorphic_type (fst (destConst f))) ->
(* Sort-polymorphism of definition and inductive types *)
goalacc,
type_of_global_reference_knowing_conclusion env sigma f conclty,
@@ -381,13 +390,19 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
mk_hdgoals sigma goal goalacc f
in
let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
- check_conv_leq_goal env sigma trm conclty' conclty;
+ let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
let ans = if applicand == f && args == l then trm else Term.mkApp (applicand, args) in
(acc'',conclty',sigma, ans)
- | Case (ci,p,c,lf) ->
+ | Proj (p,c) ->
+ let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
+ let c = mkProj (p, c') in
+ let ty = get_type_of env sigma c in
+ (acc',ty,sigma,c)
+
+ | Case (ci,p,c,lf) ->
let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
- check_conv_leq_goal env sigma trm conclty' conclty;
+ let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
let (acc'',sigma, rbranches) =
Array.fold_left2
(fun (lacc,sigma,bacc) ty fi ->
@@ -401,13 +416,12 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
in
(acc'',conclty',sigma, ans)
- | _ ->
+ | _ ->
if occur_meta trm then
anomaly (Pp.str "refiner called with a meta in non app/case subterm");
-
- let t'ty = goal_type_of env sigma trm in
- check_conv_leq_goal env sigma trm t'ty conclty;
- (goalacc,t'ty,sigma, trm)
+ let t'ty = goal_type_of env sigma trm in
+ let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
+ (goalacc,t'ty,sigma, trm)
(* Same as mkREFGOALS but without knowing the type of the term. Therefore,
* Metas should be casted. *)
@@ -454,6 +468,12 @@ and mk_hdgoals sigma goal goalacc trm =
in
(acc'',conclty',sigma, ans)
+ | Proj (p,c) ->
+ let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
+ let c = mkProj (p, c') in
+ let ty = get_type_of env sigma c in
+ (acc',ty,sigma,c)
+
| _ ->
if !check && occur_meta trm then
anomaly (Pp.str "refine called with a dependent meta");
@@ -569,12 +589,12 @@ let prim_refiner r sigma goal =
check_ind (push_rel (na,None,c1) env) (k-1) b
| _ -> error "Not enough products."
in
- let (sp,_) = check_ind env n cl in
+ let ((sp,_),u) = check_ind env n cl in
let firsts,lasts = List.chop j rest in
let all = firsts@(f,n,cl)::lasts in
let rec mk_sign sign = function
| (f,n,ar)::oth ->
- let (sp',_) = check_ind env n ar in
+ let ((sp',_),u') = check_ind env n ar in
if not (eq_mind sp sp') then
error ("Fixpoints should be on the same " ^
"mutual inductive declaration.");
@@ -652,13 +672,11 @@ let prim_refiner r sigma goal =
(* Conversion rules *)
| Convert_concl (cl',k) ->
check_typability env sigma cl';
- if (not !check) || is_conv_leq env sigma cl' cl then
- let (sg,ev,sigma) = mk_goal sign cl' in
- let ev = if k != DEFAULTcast then mkCast(ev,k,cl) else ev in
- let sigma = Goal.V82.partial_solution sigma goal ev in
+ let (sg,ev,sigma) = mk_goal sign cl' in
+ let sigma = check_conv_leq_goal env sigma cl' cl' cl in
+ let ev = if k != DEFAULTcast then mkCast(ev,k,cl) else ev in
+ let sigma = Goal.V82.partial_solution sigma goal ev in
([sg], sigma)
- else
- error "convert-concl rule passed non-converting term"
| Convert_hyp (id,copt,ty) ->
let (gl,ev,sigma) = mk_goal (convert_hyp sign sigma (id,copt,ty)) cl in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index f45eb2a3aa..3fc01c0bc1 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -118,26 +118,28 @@ open Decl_kinds
let next = let n = ref 0 in fun () -> incr n; !n
-let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac =
+let build_constant_by_tactic id sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
+ let substref = ref Univ.LMap.empty in (** FIXME: Something wrong here with subst *)
start_proof id goal_kind sign typ (fun _ -> ());
try
let status = by tac in
let _,(const,_) = cook_proof () in
delete_current_proof ();
- const, status
+ const, status, !substref
with reraise ->
let reraise = Errors.push reraise in
delete_current_proof ();
raise reraise
-let build_by_tactic env typ tac =
+let build_by_tactic env ?(poly=false) typ tac =
let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
let sign = val_of_named_context (named_context env) in
- let ce,status = build_constant_by_tactic id sign typ tac in
+ let gk = Global, poly, Proof Theorem in
+ let ce, status, subst = build_constant_by_tactic id sign ~goal_kind:gk typ tac in
let ce = Term_typing.handle_side_effects env ce in
let cb, se = Future.force ce.const_entry_body in
- assert(Declareops.side_effects_is_empty (Declareops.no_seff));
- cb,status
+ assert(Declareops.side_effects_is_empty se);
+ cb, status, subst
(**********************************************************************)
(* Support for resolution of evars in tactic interpretation, including
@@ -156,6 +158,9 @@ let solve_by_implicit_tactic env sigma evk =
when
Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps)
(Environ.named_context env) ->
- (try fst (build_by_tactic env evi.evar_concl (Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) [])))
+ let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in
+ (try
+ let (ans, _, _) = build_by_tactic env (evi.evar_concl, Evd.get_universe_context_set sigma) tac in
+ ans
with e when Logic.catchable_exception e -> raise Exit)
| _ -> raise Exit
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index fea1b701ed..877b7c8586 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -56,7 +56,7 @@ val delete_all_proofs : unit -> unit
type lemma_possible_guards = Proof_global.lemma_possible_guards
val start_proof :
- Id.t -> goal_kind -> named_context_val -> constr ->
+ Id.t -> goal_kind -> named_context_val -> constr Univ.in_universe_context_set ->
?init_tac:unit Proofview.tactic ->
Proof_global.proof_terminator -> unit
@@ -149,8 +149,10 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
val build_constant_by_tactic :
Id.t -> named_context_val -> ?goal_kind:goal_kind ->
- types -> unit Proofview.tactic -> Entries.definition_entry * bool
-val build_by_tactic : env -> types -> unit Proofview.tactic -> constr * bool
+ types Univ.in_universe_context_set -> unit Proofview.tactic -> Entries.definition_entry * bool * Universes.universe_opt_subst
+val build_by_tactic : env -> ?poly:polymorphic ->
+ types Univ.in_universe_context_set -> unit Proofview.tactic ->
+ constr * bool * Universes.universe_opt_subst
(** Declare the default tactic to fill implicit arguments *)
@@ -161,10 +163,3 @@ val clear_implicit_tactic : unit -> unit
(* Raise Exit if cannot solve *)
val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr
-
-
-
-
-
-
-
diff --git a/proofs/proof.mli b/proofs/proof.mli
index ac922ac50d..30b65d0ce9 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -51,9 +51,8 @@ val proof : proof ->
(*** General proof functions ***)
-val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof
+val start : Evd.evar_map -> (Environ.env * Term.types Univ.in_universe_context_set) list -> proof
val dependent_start : Evd.evar_map -> Proofview.telescope -> proof
-
val initial_goals : proof -> (Term.constr * Term.types) list
(* Returns [true] if the considered proof is completed, that is if no goal remain
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 3cdecb633b..7434979f8f 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -68,6 +68,7 @@ type proof_object = {
id : Names.Id.t;
entries : Entries.definition_entry list;
persistence : Decl_kinds.goal_kind;
+ opt_subst : Universes.universe_opt_subst;
}
type proof_ending =
@@ -78,6 +79,10 @@ type proof_ending =
type proof_terminator = proof_ending -> unit
type closed_proof = proof_object * proof_terminator
+type 'a proof_decl_hook =
+ Universes.universe_opt_subst Univ.in_universe_context ->
+ Decl_kinds.locality -> Globnames.global_reference -> 'a
+
type pstate = {
pid : Id.t;
terminator : proof_terminator Ephemeron.key;
@@ -264,18 +269,29 @@ let get_open_goals () =
let close_proof ?feedback_id ~now fpl =
let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
let initial_goals = Proof.initial_goals proof in
- let entries =
- Future.map2 (fun p (c, t) -> { Entries.
- const_entry_body = p;
- const_entry_secctx = section_vars;
- const_entry_feedback = feedback_id;
- const_entry_type = Some t;
- const_entry_inline_code = false;
- const_entry_opaque = true })
- fpl initial_goals in
+ let evdref = ref (Proof.return proof) in
+ let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
+ let initial_goals = List.map (fun (c,t) -> (nf c, nf t)) initial_goals in
+ let ctx = Evd.universe_context !evdref in
+ let entries = Future.map2 (fun p (c, t) ->
+ let univs =
+ Univ.LSet.union (Universes.universes_of_constr c)
+ (Universes.universes_of_constr t)
+ in
+ let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) univs in
+ { Entries.
+ const_entry_body = p;
+ const_entry_secctx = section_vars;
+ const_entry_type = Some t;
+ const_entry_feedback = feedback_id;
+ const_entry_inline_code = false;
+ const_entry_opaque = true;
+ const_entry_universes = Univ.ContextSet.to_context ctx;
+ const_entry_polymorphic = pi2 strength;
+ const_entry_proj = None}) fpl initial_goals in
if now then
- List.iter (fun x ->ignore(Future.force x.Entries.const_entry_body)) entries;
- { id = pid; entries = entries; persistence = strength },
+ List.iter (fun x -> ignore(Future.force x.Entries.const_entry_body)) entries;
+ { id = pid; entries = entries; persistence = strength; opt_subst = subst },
Ephemeron.get terminator
let return_proof () =
@@ -312,6 +328,9 @@ let set_terminator hook =
| [] -> raise NoCurrentProof
| p :: ps -> pstates := { p with terminator = Ephemeron.create hook } :: ps
+
+
+
(**********************************************************)
(* *)
(* Bullets *)
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 47d63e2ebf..e651bdfae3 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -46,6 +46,10 @@ exception NoCurrentProof
val give_me_the_proof : unit -> Proof.proof
(** @raise NoCurrentProof when outside proof mode. *)
+type 'a proof_decl_hook =
+ Universes.universe_opt_subst Univ.in_universe_context ->
+ Decl_kinds.locality -> Globnames.global_reference -> 'a
+
(** When a proof is closed, it is reified into a [proof_object], where
[id] is the name of the proof, [entries] the list of the proof terms
(in a form suitable for definitions). Together with the [terminator]
@@ -57,6 +61,7 @@ type proof_object = {
id : Names.Id.t;
entries : Entries.definition_entry list;
persistence : Decl_kinds.goal_kind;
+ opt_subst : Universes.universe_opt_subst;
}
type proof_ending =
@@ -74,7 +79,7 @@ type closed_proof = proof_object * proof_terminator
closing commands and the xml plugin); [terminator] is used at the
end of the proof to close the proof. *)
val start_proof :
- Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types) list ->
+ Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types Univ.in_universe_context_set) list ->
proof_terminator -> unit
(** Like [start_proof] except that there may be dependencies between
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 22d908e94c..d0a477431f 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -36,10 +36,11 @@ let proofview p =
let init sigma =
let rec aux = function
| [] -> [], { solution = sigma; comb = []; }
- | (env, typ) :: l ->
+ | (env, (typ,ctx)) :: l ->
let ret, { solution = sol; comb = comb } = aux l in
let (new_defs , econstr) = Evarutil.new_evar sol env typ in
let (e, _) = Term.destEvar econstr in
+ let new_defs = Evd.merge_context_set Evd.univ_rigid new_defs ctx in
let gl = Goal.build e in
let entry = (econstr, typ) :: ret in
entry, { solution = new_defs; comb = gl::comb; }
@@ -88,6 +89,12 @@ let partial_proof entry pv = List.map (return_constr pv) (List.map fst entry)
let emit_side_effects eff x =
{ x with solution = Evd.emit_side_effects eff x.solution }
+(* let return { initial=init; solution=defs } = *)
+(* let evdref = ref defs in *)
+(* let nf,subst = Evarutil.e_nf_evars_and_universes evdref in *)
+(* ((List.map (fun (c,t) -> (nf c, nf t)) init, subst), *)
+(* Evd.universe_context !evdref) *)
+
(* spiwack: this function should probably go in the Util section,
but I'd rather have Util (or a separate module for lists)
raise proper exceptions before *)
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 55d93f92e0..bfb88c897a 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -37,7 +37,7 @@ type entry
(* Initialises a proofview, the argument is a list of environement,
conclusion types, creating that many initial goals. *)
-val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview
+val init : Evd.evar_map -> (Environ.env * Term.types Univ.in_universe_context_set) list -> entry * proofview
type telescope =
| TNil
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 9a78a79fd0..663e24f9fc 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -27,6 +27,10 @@ let refiner pr goal_sigma =
let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in
{ it = sgl; sigma = sigma'; }
+(* Profiling refiner *)
+(* let refiner_key = Profile.declare_profile "refiner" *)
+(* let refiner = Profile.profile2 refiner_key refiner *)
+
(*********************)
(* Tacticals *)
(*********************)
@@ -318,6 +322,19 @@ let rec tclREPEAT_MAIN t g =
(* Change evars *)
let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
+(* Push universe context *)
+let tclPUSHCONTEXT rigid ctx tac gl =
+ tclTHEN (tclEVARS (Evd.merge_context_set rigid (project gl) ctx)) tac gl
+
+let tclPUSHEVARUNIVCONTEXT ctx gl =
+ tclEVARS (Evd.merge_universe_context (project gl) ctx) gl
+
+let tclPUSHCONSTRAINTS cst gl =
+ tclEVARS (Evd.add_constraints (project gl) cst) gl
+
+let tclPUSHUNIVERSECONSTRAINTS cst gl =
+ tclEVARS (Evd.add_universe_constraints (project gl) cst) gl
+
(* Check that holes in arguments have been resolved *)
let check_evars env sigma extsigma origsigma =
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index f73bdaf934..25ab1fb766 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -34,6 +34,12 @@ val tclIDTAC_MESSAGE : Pp.std_ppcmds -> tactic
(** [tclEVARS sigma] changes the current evar map *)
val tclEVARS : evar_map -> tactic
+val tclPUSHCONTEXT : Evd.rigid -> Univ.universe_context_set -> tactic -> tactic
+val tclPUSHEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic
+
+val tclPUSHCONSTRAINTS : Univ.constraints -> tactic
+val tclPUSHUNIVERSECONSTRAINTS : Univ.UniverseConstraints.t -> tactic
+
(** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
[tac2] to every resulting subgoals *)
val tclTHEN : tactic -> tactic -> tactic
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 855529ac28..2faf18355e 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -86,8 +86,10 @@ let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds)
let pf_type_of = pf_reduce type_of
let pf_get_type_of = pf_reduce Retyping.get_type_of
-let pf_conv_x = pf_reduce is_conv
-let pf_conv_x_leq = pf_reduce is_conv_leq
+let pf_conv_x gl = pf_reduce test_conversion gl Reduction.CONV
+let pf_conv_x_leq gl = pf_reduce test_conversion gl Reduction.CUMUL
+let pf_const_value = pf_reduce (fun env _ -> constant_value_in env)
+
let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 7bac4c6e9e..326d14bf69 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -62,12 +62,13 @@ val pf_whd_betadeltaiota : goal sigma -> constr -> constr
val pf_hnf_constr : goal sigma -> constr -> constr
val pf_nf : goal sigma -> constr -> constr
val pf_nf_betaiota : goal sigma -> constr -> constr
-val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types
-val pf_reduce_to_atomic_ind : goal sigma -> types -> inductive * types
+val pf_reduce_to_quantified_ind : goal sigma -> types -> pinductive * types
+val pf_reduce_to_atomic_ind : goal sigma -> types -> pinductive * types
val pf_compute : goal sigma -> constr -> constr
val pf_unfoldn : (occurrences * evaluable_global_reference) list
-> goal sigma -> constr -> constr
+val pf_const_value : goal sigma -> pconstant -> constr
val pf_conv_x : goal sigma -> constr -> constr -> bool
val pf_conv_x_leq : goal sigma -> constr -> constr -> bool
@@ -125,7 +126,7 @@ module New : sig
val pf_last_hyp : [ `NF ] Proofview.Goal.t -> named_declaration
val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types
- val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> inductive * types
+ val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> pinductive * types
val pf_hnf_constr : 'a Proofview.Goal.t -> constr -> types
val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 03:08:02 +0000