aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/class.ml1
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/comAssumption.ml3
-rw-r--r--vernac/comAssumption.mli4
-rw-r--r--vernac/comDefinition.ml4
-rw-r--r--vernac/comFixpoint.ml3
-rw-r--r--vernac/comInductive.ml2
-rw-r--r--vernac/comProgramFixpoint.ml8
-rw-r--r--vernac/himsg.ml23
-rw-r--r--vernac/obligations.ml11
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/vernacentries.ml26
-rw-r--r--vernac/vernacprop.ml1
13 files changed, 42 insertions, 50 deletions
diff --git a/vernac/class.ml b/vernac/class.ml
index 59d933108..f0b01061b 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -181,6 +181,7 @@ let build_id_coercion idf_opt source poly =
let sigma, vs = match source with
| CL_CONST sp -> Evd.fresh_global env sigma (ConstRef sp)
| _ -> error_not_transparent source in
+ let vs = EConstr.Unsafe.to_constr vs in
let c = match constant_opt_value_in env (destConst vs) with
| Some c -> c
| None -> error_not_transparent source in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 76d427add..7f2642093 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -293,7 +293,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
(* Check that the type is free of evars now. *)
Pretyping.check_evars env Evd.empty sigma termtype;
let termtype = to_constr sigma termtype in
- let term = Option.map (to_constr sigma) term in
+ let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
if not (Evd.has_undefined sigma) && not (Option.is_empty term) then
declare_instance_constant k pri global imps ?hook id decl
poly sigma (Option.get term) termtype
@@ -425,7 +425,7 @@ let context poly l =
let nstatus = match b with
| None ->
pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl
- Vernacexpr.NoInline (CAst.make id))
+ Declaremods.NoInline (CAst.make id))
| Some b ->
let decl = (Discharge, poly, Definition) in
let entry = Declare.definition_entry ~univs ~types:t b in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 6a590758f..26a46a752 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -20,7 +20,6 @@ open Constrintern
open Impargs
open Decl_kinds
open Pretyping
-open Vernacexpr
open Entries
(* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
@@ -66,7 +65,7 @@ match local with
| Global | Local | Discharge ->
let do_instance = should_axiom_into_instance local in
let local = DeclareDef.get_locality ident ~kind:"axiom" local in
- let inl = match nl with
+ let inl = let open Declaremods in match nl with
| NoInline -> None
| DefaultInline -> Some (Flags.get_inline_level())
| InlineAt i -> Some i
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 56e324376..a2d20a1d1 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -19,7 +19,7 @@ open Decl_kinds
(** {6 Parameters/Assumptions} *)
val do_assumptions : locality * polymorphic * assumption_object_kind ->
- Vernacexpr.inline -> (ident_decl list * constr_expr) with_coercion list -> bool
+ Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list -> bool
(************************************************************************)
(** Internal API *)
@@ -32,5 +32,5 @@ val do_assumptions : locality * polymorphic * assumption_object_kind ->
val declare_assumption : coercion_flag -> assumption_kind ->
types in_constant_universes_entry ->
Universes.universe_binders -> Impargs.manual_implicits ->
- bool (** implicit *) -> Vernacexpr.inline -> variable CAst.t ->
+ bool (** implicit *) -> Declaremods.inline -> variable CAst.t ->
global_reference * Univ.Instance.t * bool
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index b18a60a1f..9aa61ab46 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -88,8 +88,8 @@ let interp_definition pl bl poly red_option c ctypopt =
let evd = Evd.minimize_universes evd in
(* Substitute evars and universes, and add parameters.
Note: in program mode some evars may remain. *)
- let ctx = List.map (EConstr.to_rel_decl evd) ctx in
- let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr evd c) ctx in
+ let ctx = List.map Termops.(map_rel_decl (to_constr ~abort_on_undefined_evars:false evd)) ctx in
+ let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd c) ctx in
let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr evd ty) ctx) tyopt in
(* Keep only useful universes. *)
let uvars_fold uvars c =
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index a794c2db0..1466fa243 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -225,7 +225,8 @@ let interp_recursive ~program_mode ~cofix fixl notations =
(* Instantiate evars and check all are resolved *)
let sigma = solve_unif_constraints_with_heuristics env_rec sigma in
let sigma, _ = nf_evars_and_universes sigma in
- let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr sigma) c) fixdefs in
+ (* XXX: We still have evars here in Program *)
+ let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr ~abort_on_undefined_evars:false sigma) c) fixdefs in
let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in
let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index db2f16525..05c40dbdd 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -261,7 +261,7 @@ let check_param = function
| CLocalAssum (nas, Default _, _) -> List.iter check_named nas
| CLocalAssum (nas, Generalized _, _) -> ()
| CLocalPattern {CAst.loc} ->
- Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.")
+ Loc.raise ?loc (Stream.Error "pattern with quote not allowed here")
let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
check_all_names_different indl;
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index b95741ca4..745f1df1d 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -229,7 +229,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
in
(* XXX: Capturing sigma here... bad bad *)
let hook = Lemmas.mk_hook (hook sigma) in
- let fullcoqc = EConstr.to_constr sigma def in
+ (* XXX: Grounding non-ground terms here... bad bad *)
+ let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in
let fullctyp = EConstr.to_constr sigma typ in
Obligations.check_evars env sigma;
let evars, _, evars_def, evars_typ =
@@ -261,9 +262,10 @@ let do_program_recursive local poly fixkind fixl ntns =
let collect_evars id def typ imps =
(* Generalize by the recursive prototypes *)
let def =
- EConstr.to_constr evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)
+ EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)
and typ =
- EConstr.to_constr evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)
+ (* Worrying... *)
+ EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)
in
let evm = collect_evars_of_term evd def typ in
let evars, _, def, typ =
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 698ee4703..acb461cac 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -75,11 +75,7 @@ let rec contract3' env sigma a b c = function
| MetaOccurInBody _ | InstanceNotSameType _ | ProblemBeyondCapabilities
| UnifUnivInconsistency _ as x -> contract3 env sigma a b c, x
| CannotSolveConstraint ((pb,env',t,u),x) ->
- let t = EConstr.of_constr t in
- let u = EConstr.of_constr u in
let env',t,u = contract2 env' sigma t u in
- let t = EConstr.Unsafe.to_constr t in
- let u = EConstr.Unsafe.to_constr u in
let y,x = contract3' env sigma a b c x in
y,CannotSolveConstraint ((pb,env',t,u),x)
@@ -322,8 +318,6 @@ let explain_unification_error env sigma p1 p2 = function
else
[str "universe inconsistency"]
| CannotSolveConstraint ((pb,env,t,u),e) ->
- let t = EConstr.of_constr t in
- let u = EConstr.of_constr u in
let env = make_all_name_different env sigma in
(strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++
str " == " ++ pr_leconstr_env env sigma u)
@@ -562,9 +556,9 @@ let rec explain_evar_kind env sigma evk ty = function
| Evar_kinds.SubEvar (where,evk') ->
let evi = Evd.find sigma evk' in
let pc = match evi.evar_body with
- | Evar_defined c -> pr_leconstr_env env sigma (EConstr.of_constr c)
+ | Evar_defined c -> pr_leconstr_env env sigma c
| Evar_empty -> assert false in
- let ty' = EConstr.of_constr evi.evar_concl in
+ let ty' = evi.evar_concl in
(match where with
| Some Evar_kinds.Body -> str "the body of "
| Some Evar_kinds.Domain -> str "the domain of "
@@ -577,11 +571,11 @@ let rec explain_evar_kind env sigma evk ty = function
(pr_leconstr_env env sigma ty') (snd evi.evar_source)
let explain_typeclass_resolution env sigma evi k =
- match Typeclasses.class_of_constr sigma (EConstr.of_constr evi.evar_concl) with
+ match Typeclasses.class_of_constr sigma evi.evar_concl with
| Some _ ->
let env = Evd.evar_filtered_env evi in
fnl () ++ str "Could not find an instance for " ++
- pr_lconstr_env env sigma evi.evar_concl ++
+ pr_leconstr_env env sigma evi.evar_concl ++
pr_trailing_ne_context_of env sigma
| _ -> mt()
@@ -590,14 +584,14 @@ let explain_placeholder_kind env sigma c e =
| Some (SeveralInstancesFound n) ->
strbrk " (several distinct possible type class instances found)"
| None ->
- match Typeclasses.class_of_constr sigma (EConstr.of_constr c) with
+ match Typeclasses.class_of_constr sigma c with
| Some _ -> strbrk " (no type class instance found)"
| _ -> mt ()
let explain_unsolvable_implicit env sigma evk explain =
let evi = Evarutil.nf_evar_info sigma (Evd.find_undefined sigma evk) in
let env = Evd.evar_filtered_env evi in
- let type_of_hole = pr_lconstr_env env sigma evi.evar_concl in
+ let type_of_hole = pr_leconstr_env env sigma evi.evar_concl in
let pe = pr_trailing_ne_context_of env sigma in
strbrk "Cannot infer " ++
explain_evar_kind env sigma evk type_of_hole (snd evi.evar_source) ++
@@ -640,8 +634,7 @@ let explain_refiner_cannot_generalize env sigma ty =
pr_leconstr_env env sigma ty ++ str "."
let explain_no_occurrence_found env sigma c id =
- let c = EConstr.to_constr sigma c in
- str "Found no subterm matching " ++ pr_lconstr_env env sigma c ++
+ str "Found no subterm matching " ++ pr_leconstr_env env sigma c ++
str " in " ++
(match id with
| Some id -> Id.print id
@@ -766,7 +759,7 @@ let pr_constraints printenv env sigma evars cstrs =
let evs =
prlist
(fun (ev, evi) -> fnl () ++ pr_existential_key sigma ev ++
- str " : " ++ pr_lconstr_env env' sigma evi.evar_concl ++ fnl ()) l
+ str " : " ++ pr_leconstr_env env' sigma evi.evar_concl ++ fnl ()) l
in
h 0 (pe ++ evs ++ pr_evar_constraints sigma cstrs)
else
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 064e40b9b..3f2792518 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -209,8 +209,10 @@ let eterm_obligations env name evm fs ?status t ty =
List.fold_right
(fun (id, (n, nstr), ev) l ->
let hyps = Evd.evar_filtered_context ev in
- let hyps = trunc_named_context nc_len hyps in
- let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in
+ let hyps = trunc_named_context nc_len hyps in
+ let hyps = EConstr.Unsafe.to_named_context hyps in
+ let concl = EConstr.Unsafe.to_constr ev.evar_concl in
+ let evtyp, deps, transp = etype_of_evar l hyps concl in
let evtyp, hyps, chop =
match chop_product fs evtyp with
| Some t -> t, trunc_named_context fs hyps, fs
@@ -356,7 +358,7 @@ let _ =
optread = get_shrink_obligations;
optwrite = set_shrink_obligations; }
-let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
+let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type)
let get_obligation_body expand obl =
match obl.obl_body with
@@ -813,10 +815,9 @@ let rec string_of_list sep f = function
let solve_by_tac name evi t poly ctx =
let id = name in
- let concl = EConstr.of_constr evi.evar_concl in
(* spiwack: the status is dropped. *)
let (entry,_,ctx') = Pfedit.build_constant_by_tactic
- id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
+ id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl (Tacticals.New.tclCOMPLETE t) in
let env = Global.env () in
let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
let body, () = Future.force entry.const_entry_body in
diff --git a/vernac/record.ml b/vernac/record.ml
index 6e745b2af..78e68e8a3 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -114,7 +114,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
(function CLocalDef (b, _, _) -> error default_binder_kind b
| CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls
| CLocalPattern {CAst.loc} ->
- Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps
+ Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps
in
let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars env0 sigma ps in
let sigma, typ, sort, template = match t with
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 503a22f54..8c48490ff 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -449,7 +449,7 @@ let start_proof_and_print k l hook =
let evi = Evarutil.nf_evar_info sigma evi in
let env = Evd.evar_filtered_env evi in
try
- let concl = EConstr.of_constr evi.Evd.evar_concl in
+ let concl = evi.Evd.evar_concl in
if not (Evarutil.is_ground_env sigma env &&
Evarutil.is_ground_term sigma concl)
then raise Exit;
@@ -534,17 +534,14 @@ let vernac_assumption ~atts discharge kind l nl =
if not status then Feedback.feedback Feedback.AddedAxiom
let should_treat_as_cumulative cum poly =
- if poly then
- match cum with
- | GlobalCumulativity | LocalCumulativity -> true
- | GlobalNonCumulativity | LocalNonCumulativity -> false
- else
- match cum with
- | GlobalCumulativity | GlobalNonCumulativity -> false
- | LocalCumulativity ->
- user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.")
- | LocalNonCumulativity ->
- user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
+ match cum with
+ | Some VernacCumulative ->
+ if poly then true
+ else user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.")
+ | Some VernacNonCumulative ->
+ if poly then false
+ else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
+ | None -> poly && Flags.is_polymorphic_inductive_cumulativity ()
let vernac_record cum k poly finite struc binders sort nameopt cfs =
let is_cumulative = should_treat_as_cumulative cum poly in
@@ -565,7 +562,6 @@ let vernac_record cum k poly finite struc binders sort nameopt cfs =
indicates whether the type is inductive, co-inductive or
neither. *)
let vernac_inductive ~atts cum lo finite indl =
- let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
if Dumpglob.dump () then
List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
match cstrs with
@@ -602,6 +598,7 @@ let vernac_inductive ~atts cum lo finite indl =
| _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.")
in
let indl = List.map unpack indl in
+ let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite
let vernac_fixpoint ~atts discharge l =
@@ -675,7 +672,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
else (idl,ty)) binders_ast in
let mp =
Declaremods.declare_module Modintern.interp_module_ast
- id binders_ast (Enforce mty_ast) []
+ id binders_ast (Declaremods.Enforce mty_ast) []
in
Dumpglob.dump_moddef ?loc mp "mod";
Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
@@ -2008,7 +2005,6 @@ let interp ?proof ~atts ~st c =
| VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command")
| VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command")
| VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command")
- | VernacBacktrack _ -> CErrors.user_err (str "Backtrack cannot be used through the Load command")
(* Resetting *)
| VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.")
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index a837b77a3..0fdd2faaf 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -31,7 +31,6 @@ let rec has_Fail = function
let is_navigation_vernac_expr = function
| VernacResetInitial
| VernacResetName _
- | VernacBacktrack _
| VernacBackTo _
| VernacBack _ -> true
| _ -> false
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 23:23:13 +0000