aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--azure-pipelines.yml4
-rw-r--r--coq.opam5
-rw-r--r--doc/plugin_tutorial/tuto1/src/simple_declare.ml13
-rw-r--r--plugins/ltac/g_auto.mlg11
-rw-r--r--plugins/ltac/g_tactic.mlg6
-rw-r--r--plugins/ltac/pptactic.ml5
-rw-r--r--plugins/ltac/tacexpr.ml3
-rw-r--r--plugins/ltac/tacexpr.mli3
-rw-r--r--plugins/ltac/tacintern.ml8
-rw-r--r--plugins/ltac/tacinterp.ml8
-rw-r--r--plugins/ltac/tacsubst.ml4
-rw-r--r--tactics/tactics.ml51
-rw-r--r--tactics/tactics.mli8
-rw-r--r--test-suite/bugs/closed/bug_10025.v39
-rw-r--r--test-suite/success/change.v8
-rw-r--r--vernac/comDefinition.ml31
16 files changed, 129 insertions, 78 deletions
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index f09087b172..f2cec1eb19 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -59,8 +59,8 @@ jobs:
- script: |
set -e
export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig
- opam init -a -j "$NJOBS" --compiler=$COMPILER
- opam switch set $COMPILER
+ opam init -a -j "$NJOBS" --compiler=ocaml-base-compiler.$COMPILER
+ opam switch set ocaml-base-compiler.$COMPILER
eval $(opam env)
opam update
opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3
diff --git a/coq.opam b/coq.opam
index da3f1b518d..05b20e08b6 100644
--- a/coq.opam
+++ b/coq.opam
@@ -25,11 +25,8 @@ depends: [
"num"
]
-build-env: [
- [ COQ_CONFIGURE_PREFIX = "%{prefix}" ]
-]
-
build: [
+ [ "./configure" "-prefix" prefix "-native-compiler" "no" ]
[ "dune" "build" "@vodeps" ]
[ "dune" "exec" "coq_dune" "_build/default/.vfiles.d" ]
[ "dune" "build" "-p" name "-j" jobs ]
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 23f8fbe888..3c0355c92d 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,17 +1,8 @@
-(* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *)
let edeclare ?hook ~ontop ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
- let sigma = Evd.minimize_universes sigma in
- let body = EConstr.to_constr sigma body in
- let tyopt = Option.map (EConstr.to_constr sigma) tyopt in
- let uvars_fold uvars c =
- Univ.LSet.union uvars (Vars.universes_of_constr c) in
- let uvars = List.fold_left uvars_fold Univ.LSet.empty
- (Option.List.cons tyopt [body]) in
- let sigma = Evd.restrict_universe_context sigma uvars in
- let univs = Evd.check_univ_decl ~poly sigma udecl in
+ let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false
+ ~opaque ~poly sigma udecl ~types:tyopt ~body in
let uctx = Evd.evar_universe_context sigma in
let ubinders = Evd.universe_binders sigma in
- let ce = Declare.definition_entry ?types:tyopt ~univs body in
let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
DeclareDef.declare_definition ~ontop ident k ce ubinders imps ?hook_data
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index ec5e46d89b..e59076bd63 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -182,9 +182,18 @@ TACTIC EXTEND unify
}
END
+{
+let deprecated_convert_concl_no_check =
+ CWarnings.create
+ ~name:"convert_concl_no_check" ~category:"deprecated"
+ (fun () -> Pp.str "The syntax [convert_concl_no_check] is deprecated. Use [change_no_check] instead.")
+}
TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl ~check:false x DEFAULTcast }
+| ["convert_concl_no_check" constr(x) ] -> {
+ deprecated_convert_concl_no_check ();
+ Tactics.convert_concl ~check:false x DEFAULTcast
+ }
END
{
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index a2dd51643b..c23240b782 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -703,7 +703,11 @@ GRAMMAR EXTEND Gram
| IDENT "change"; c = conversion; cl = clause_dft_concl ->
{ let (oc, c) = c in
let p,cl = merge_occurrences loc cl oc in
- TacAtom (CAst.make ~loc @@ TacChange (p,c,cl)) }
+ TacAtom (CAst.make ~loc @@ TacChange (true,p,c,cl)) }
+ | IDENT "change_no_check"; c = conversion; cl = clause_dft_concl ->
+ { let (oc, c) = c in
+ let p,cl = merge_occurrences loc cl oc in
+ TacAtom (CAst.make ~loc @@ TacChange (false,p,c,cl)) }
] ]
;
END
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 80070a7493..79f0f521cc 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -833,9 +833,10 @@ let pr_goal_selector ~toplevel s =
pr_red_expr r
++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
)
- | TacChange (op,c,h) ->
+ | TacChange (check,op,c,h) ->
+ let name = if check then "change_no_check" else "change" in
hov 1 (
- primitive "change" ++ brk (1,1)
+ primitive name ++ brk (1,1)
++ (
match op with
None ->
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 30e316b36d..0eb7726a18 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -34,6 +34,7 @@ type rec_flag = bool (* true = recursive false = not recursive *)
type advanced_flag = bool (* true = advanced false = basic *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+type check_flag = bool (* true = check false = do not check *)
type ('c,'d,'id) inversion_strength =
| NonDepInversion of
@@ -125,7 +126,7 @@ type 'a gen_atomic_tactic_expr =
(* Conversion *)
| TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
- | TacChange of 'pat option * 'dtrm * 'nam clause_expr
+ | TacChange of check_flag * 'pat option * 'dtrm * 'nam clause_expr
(* Equality and inversion *)
| TacRewrite of evars_flag *
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 8b6b14322b..fd303f5d94 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -34,6 +34,7 @@ type rec_flag = bool (* true = recursive false = not recursive *)
type advanced_flag = bool (* true = advanced false = basic *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+type check_flag = bool (* true = check false = do not check *)
type ('c,'d,'id) inversion_strength =
| NonDepInversion of
@@ -124,7 +125,7 @@ type 'a gen_atomic_tactic_expr =
(* Conversion *)
| TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
- | TacChange of 'pat option * 'dtrm * 'nam clause_expr
+ | TacChange of check_flag * 'pat option * 'dtrm * 'nam clause_expr
(* Equality and inversion *)
| TacRewrite of evars_flag *
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 543d4de0fe..c1f7fab123 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -551,7 +551,7 @@ let rec intern_atomic lf ist x =
| TacReduce (r,cl) ->
dump_glob_red_expr r;
TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl)
- | TacChange (None,c,cl) ->
+ | TacChange (check,None,c,cl) ->
let is_onhyps = match cl.onhyps with
| None | Some [] -> true
| _ -> false
@@ -560,17 +560,17 @@ let rec intern_atomic lf ist x =
| AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
| _ -> false
in
- TacChange (None,
+ TacChange (check,None,
(if is_onhyps && is_onconcl
then intern_type ist c else intern_constr ist c),
clause_app (intern_hyp_location ist) cl)
- | TacChange (Some p,c,cl) ->
+ | TacChange (check,Some p,c,cl) ->
let { ltacvars } = ist in
let metas,pat = intern_typed_pattern ist ~as_type:false ~ltacvars p in
let fold accu x = Id.Set.add x accu in
let ltacvars = List.fold_left fold ltacvars metas in
let ist' = { ist with ltacvars } in
- TacChange (Some pat,intern_constr ist' c,
+ TacChange (check,Some pat,intern_constr ist' c,
clause_app (intern_hyp_location ist) cl)
(* Equality and inversion *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 4398fb14ab..800be2565d 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1770,7 +1770,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl))
end
- | TacChange (None,c,cl) ->
+ | TacChange (check,None,c,cl) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<change>") begin
Proofview.Goal.enter begin fun gl ->
@@ -1792,10 +1792,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
then interp_type ist env sigma c
else interp_constr ist env sigma c
in
- Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)
+ Tactics.change ~check None c_interp (interp_clause ist (pf_env gl) (project gl) cl)
end
end
- | TacChange (Some op,c,cl) ->
+ | TacChange (check,Some op,c,cl) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<change>") begin
Proofview.Goal.enter begin fun gl ->
@@ -1815,7 +1815,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
with e when to_catch e (* Hack *) ->
user_err (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
in
- Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)
+ Tactics.change ~check (Some op) c_interp (interp_clause ist env sigma cl)
end
end
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index e617f3d45e..a3eeca2267 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -158,8 +158,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* Conversion *)
| TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
- | TacChange (op,c,cl) ->
- TacChange (Option.map (subst_glob_constr_or_pattern subst) op,
+ | TacChange (check,op,c,cl) ->
+ TacChange (check,Option.map (subst_glob_constr_or_pattern subst) op,
subst_glob_constr subst c, cl)
(* Equality and inversion *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b70dd63211..35b3b38298 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -802,15 +802,21 @@ let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
| Some sigma -> (sigma, t')
(* Use cumulativity only if changing the conclusion not a subterm *)
-let change_on_subterm cv_pb deep t where env sigma c =
+let change_on_subterm check cv_pb deep t where env sigma c =
let mayneedglobalcheck = ref false in
let (sigma, c) = match where with
- | None -> change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c
+ | None ->
+ if check then
+ change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c
+ else
+ t Id.Map.empty env sigma
| Some occl ->
e_contextually false occl
(fun subst ->
- change_and_check Reduction.CONV mayneedglobalcheck true (t subst))
- env sigma c in
+ if check then
+ change_and_check Reduction.CONV mayneedglobalcheck true (t subst)
+ else
+ fun env sigma _c -> t subst env sigma) env sigma c in
if !mayneedglobalcheck then
begin
try ignore (Typing.unsafe_type_of env sigma c)
@@ -819,14 +825,15 @@ let change_on_subterm cv_pb deep t where env sigma c =
end;
(sigma, c)
-let change_in_concl occl t =
- e_change_in_concl ~check:false ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast)
+let change_in_concl ?(check=true) occl t =
+ (* No need to check in e_change_in_concl, the check is done in change_on_subterm *)
+ e_change_in_concl ~check:false ((change_on_subterm check Reduction.CUMUL false t occl),DEFAULTcast)
-let change_in_hyp occl t id =
+let change_in_hyp ?(check=true) occl t id =
(* FIXME: we set the [check] flag only to reorder hypotheses in case of
introduction of dependencies in new variables. We should separate this
check from the conversion function. *)
- e_change_in_hyp ~check:true (fun x -> change_on_subterm Reduction.CONV x t occl) id
+ e_change_in_hyp ~check:true (fun x -> change_on_subterm check Reduction.CONV x t occl) id
let concrete_clause_of enum_hyps cl = match cl.onhyps with
| None ->
@@ -835,24 +842,24 @@ let concrete_clause_of enum_hyps cl = match cl.onhyps with
| Some l ->
List.map (fun ((occs, id), w) -> (id, occs, w)) l
-let change chg c cls =
+let change ?(check=true) chg c cls =
Proofview.Goal.enter begin fun gl ->
let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in
begin match cls.concl_occs with
| NoOccurrences -> Proofview.tclUNIT ()
- | occs -> change_in_concl (bind_change_occurrences occs chg) c
+ | occs -> change_in_concl ~check (bind_change_occurrences occs chg) c
end
<*>
let f (id, occs, where) =
let occl = bind_change_occurrences occs chg in
- let redfun deep env sigma t = change_on_subterm Reduction.CONV deep c occl env sigma t in
+ let redfun deep env sigma t = change_on_subterm check Reduction.CONV deep c occl env sigma t in
(redfun, id, where)
in
e_change_in_hyps ~check:true f hyps
end
let change_concl t =
- change_in_concl None (make_change_arg t)
+ change_in_concl ~check:true None (make_change_arg t)
(* Pour usage interne (le niveau User est pris en compte par reduce) *)
let red_in_concl = reduct_in_concl (red_product,REVERTcast)
@@ -2856,17 +2863,21 @@ let generalize_dep ?(with_let=false) c =
| _ -> tothin
in
let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
- let body =
- if with_let then
- match EConstr.kind sigma c with
- | Var id -> id |> (fun id -> pf_get_hyp id gl) |> NamedDecl.get_value
- | _ -> None
- else None
+ let is_var, body = match EConstr.kind sigma c with
+ | Var id ->
+ let body = NamedDecl.get_value (pf_get_hyp id gl) in
+ let is_var = Option.is_empty body && not (List.mem id init_ids) in
+ if with_let then is_var, body else is_var, None
+ | _ -> false, None
in
let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous)
(cl',project gl) in
(* Check that the generalization is indeed well-typed *)
- let (evd, _) = Typing.type_of env evd cl'' in
+ let evd =
+ (* No need to retype for variables, term is statically well-typed *)
+ if is_var then evd
+ else fst (Typing.type_of env evd cl'')
+ in
let args = Context.Named.to_instance mkVar to_quantify_rev in
tclTHENLIST
[ Proofview.Unsafe.tclEVARS evd;
@@ -3280,7 +3291,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
if Int.equal i nparams then
let t = applist (hd, params@args) in
Tacticals.New.tclTHEN
- (change_in_hyp None (make_change_arg t) (hyp0,InHypTypeOnly))
+ (change_in_hyp ~check:false None (make_change_arg t) (hyp0,InHypTypeOnly))
(tac avoid)
else
let c = List.nth argl (i-1) in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index e7b95a820e..b3914816ac 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -155,10 +155,10 @@ val make_change_arg : constr -> change_arg
val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic
val reduct_in_concl : ?check:bool -> tactic_reduction * cast_kind -> unit Proofview.tactic
-val e_reduct_in_concl : ?check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic
-val change_in_concl : (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic
+val e_reduct_in_concl : ?check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic
+val change_in_concl : ?check:bool -> (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic
val change_concl : constr -> unit Proofview.tactic
-val change_in_hyp : (occurrences * constr_pattern) option -> change_arg ->
+val change_in_hyp : ?check:bool -> (occurrences * constr_pattern) option -> change_arg ->
hyp_location -> unit Proofview.tactic
val red_in_concl : unit Proofview.tactic
val red_in_hyp : hyp_location -> unit Proofview.tactic
@@ -180,7 +180,7 @@ val unfold_in_hyp :
val unfold_option :
(occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic
val change :
- constr_pattern option -> change_arg -> clause -> unit Proofview.tactic
+ ?check:bool -> constr_pattern option -> change_arg -> clause -> unit Proofview.tactic
val pattern_option :
(occurrences * constr) list -> goal_location -> unit Proofview.tactic
val reduce : red_expr -> clause -> unit Proofview.tactic
diff --git a/test-suite/bugs/closed/bug_10025.v b/test-suite/bugs/closed/bug_10025.v
new file mode 100644
index 0000000000..1effc771b0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10025.v
@@ -0,0 +1,39 @@
+Require Import Program.
+
+Axiom I : Type.
+
+Inductive S : Type := NT : I -> S.
+
+Axiom F : S -> Type.
+
+Axiom G : forall (s : S), F s -> Type.
+
+Section S.
+
+Variable init : I.
+Variable my_s : F (NT init).
+
+Inductive foo : forall (s: S) (hole_sem: F s), Type :=
+| Foo : foo (NT init) my_s.
+
+Goal forall
+ (n : I) (s : F (NT n)) (ptz : foo (NT n) s) (pt : G (NT n) s) (x : unit),
+match
+ match x with tt => tt end
+with
+| tt =>
+ match
+ match ptz in foo x s return (forall _ : G x s, unit) with
+ | Foo => fun _ : G (NT init) my_s => tt
+ end pt
+ with
+ | tt => False
+ end
+end.
+Proof.
+dependent destruction ptz.
+(* Check well-typedness of goal *)
+match goal with [ |- ?P ] => let t := type of P in idtac end.
+Abort.
+
+End S.
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index a9821b027f..5a8f735151 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -68,3 +68,11 @@ eassumption.
match goal with |- ?x=1 => change (x=1) with (0+x=1) end.
match goal with |- 0+1=1 => trivial end.
Qed.
+
+(* Mini-check that no_check does not check *)
+
+Goal False.
+change_no_check True.
+exact I.
+Fail Qed.
+Abort.
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index feaf47df18..12df3215ad 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -12,7 +12,6 @@ open Pp
open Util
open Entries
open Redexpr
-open Declare
open Constrintern
open Pretyping
@@ -42,10 +41,9 @@ let check_imps ~impsty ~impsbody =
if not b then warn_implicits_in_term ()
let interp_definition ~program_mode pl bl poly red_option c ctypopt =
- let open EConstr in
let env = Global.env() in
(* Explicitly bound universes and constraints *)
- let evd, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
+ let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in
(* Build the parameters *)
let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode env evd bl in
(* Build the type *)
@@ -66,24 +64,15 @@ let interp_definition ~program_mode pl bl poly red_option c ctypopt =
in
(* Do the reduction *)
let evd, c = red_constant_body red_option env_bl evd c in
- (* universe minimization *)
- 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 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 ~abort_on_undefined_evars:false evd ty) ctx) tyopt in
- (* Keep only useful universes. *)
- let uvars_fold uvars c =
- Univ.LSet.union uvars (universes_of_constr evd (of_constr c))
- in
- let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in
- let evd = Evd.restrict_universe_context evd uvars in
- (* Check we conform to declared universes *)
- let uctx = Evd.check_univ_decl ~poly evd decl in
- (* We're done! *)
- let ce = definition_entry ?types:tyopt ~univs:uctx c in
- (ce, evd, decl, imps)
+
+ (* Declare the definition *)
+ let c = EConstr.it_mkLambda_or_LetIn c ctx in
+ let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in
+
+ let evd, ce = DeclareDef.prepare_definition ~allow_evars:program_mode
+ ~opaque:false ~poly evd udecl ~types:tyopt ~body:c in
+
+ (ce, evd, udecl, imps)
let check_definition ~program_mode (ce, evd, _, imps) =
let env = Global.env () in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 01:32:45 +0000