aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml9
-rw-r--r--vernac/classes.ml28
-rw-r--r--vernac/comTactic.ml6
-rw-r--r--vernac/comTactic.mli9
-rw-r--r--vernac/declare.ml114
-rw-r--r--vernac/himsg.ml4
-rw-r--r--vernac/indschemes.ml2
-rw-r--r--vernac/recLemmas.ml4
-rw-r--r--vernac/record.ml23
9 files changed, 92 insertions, 107 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 7a7e7d6e35..f715459616 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -145,7 +145,7 @@ let build_beq_scheme_deps kn =
| Cast (x,_,_) -> aux accu (Term.applist (x,a))
| App _ -> assert false
| Ind ((kn', _), _) ->
- if MutInd.equal kn kn' then accu
+ if Environ.QMutInd.equal env kn kn' then accu
else
let eff = SchemeMutualDep (kn', !beq_scheme_kind_aux ()) in
List.fold_left aux (eff :: accu) a
@@ -253,7 +253,7 @@ let build_beq_scheme mode kn =
| Cast (x,_,_) -> aux (Term.applist (x,a))
| App _ -> assert false
| Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
- if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
+ if Environ.QMutInd.equal env kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
else begin
try
let eq = match lookup_scheme (!beq_scheme_kind_aux()) ind' with
@@ -496,7 +496,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let u,v = try destruct_ind env sigma tt1
(* trick so that the good sequence is returned*)
with e when CErrors.noncritical e -> indu,[||]
- in if eq_ind (fst u) ind
+ in if Ind.CanOrd.equal (fst u) ind
then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ]
else (
find_scheme bl_scheme_key (fst u) (*FIXME*) >>= fun c ->
@@ -539,7 +539,8 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
end
end >>= fun (sp2,i2) ->
- if not (MutInd.equal sp1 sp2) || not (Int.equal i1 i2)
+ Proofview.tclENV >>= fun env ->
+ if not (Environ.QMutInd.equal env sp1 sp2) || not (Int.equal i1 i2)
then Tacticals.New.tclZEROMSG (str "Eq should be on the same type")
else aux (Array.to_list ca1) (Array.to_list ca2)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index a464eab127..d5509e2697 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -152,9 +152,6 @@ let subst_class (subst,cl) =
and do_subst c = Mod_subst.subst_mps subst c
and do_subst_gr gr = fst (subst_global subst gr) in
let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in
- let do_subst_context (grs,ctx) =
- List.Smart.map (Option.Smart.map do_subst_gr) grs,
- do_subst_ctx ctx in
let do_subst_meth m =
let c = Option.Smart.map do_subst_con m.meth_const in
if c == m.meth_const then m
@@ -168,7 +165,7 @@ let subst_class (subst,cl) =
let do_subst_projs projs = List.Smart.map do_subst_meth projs in
{ cl_univs = cl.cl_univs;
cl_impl = do_subst_gr cl.cl_impl;
- cl_context = do_subst_context cl.cl_context;
+ cl_context = do_subst_ctx cl.cl_context;
cl_props = do_subst_ctx cl.cl_props;
cl_projs = do_subst_projs cl.cl_projs;
cl_strict = cl.cl_strict;
@@ -197,25 +194,16 @@ let discharge_class (_,cl) =
| VarRef _ | ConstructRef _ -> assert false
| ConstRef cst -> Lib.section_segment_of_constant cst
| IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind in
- let discharge_context ctx' subst (grs, ctx) =
- let env = Global.env () in
- let sigma = Evd.from_env env in
- let grs' =
- let newgrs = List.map (fun decl ->
- match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr env sigma with
- | None -> None
- | Some (_, ((tc,_), _)) -> Some tc.cl_impl)
- ctx'
- in
- grs @ newgrs
- in grs', discharge_rel_context subst 1 ctx @ ctx' in
+ let discharge_context ctx' subst ctx =
+ discharge_rel_context subst 1 ctx @ ctx'
+ in
try
let info = abs_context cl in
let ctx = info.Section.abstr_ctx in
let ctx, subst = rel_of_variable_context ctx in
let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
let context = discharge_context ctx (subst, usubst) cl.cl_context in
- let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in
+ let props = discharge_rel_context (subst, usubst) (succ (List.length cl.cl_context)) cl.cl_props in
let discharge_proj x = x in
{ cl_univs = cl_univs';
cl_impl = cl.cl_impl;
@@ -324,7 +312,7 @@ let declare_instance_constant iinfo global impargs ?hook name udecl poly sigma t
let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name =
let subst = List.fold_left2
(fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
- [] subst (snd k.cl_context)
+ [] subst k.cl_context
in
let (_, ty_constr) = instance_constructor (k,u) subst in
let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
@@ -399,7 +387,7 @@ let do_instance_subst_constructor_and_ty subst k u ctx =
let subst =
List.fold_left2 (fun subst' s decl ->
if is_local_assum decl then s :: subst' else subst')
- [] subst (k.cl_props @ snd k.cl_context)
+ [] subst (k.cl_props @ k.cl_context)
in
let (app, ty_constr) = instance_constructor (k,u) subst in
let termtype = it_mkProd_or_LetIn ty_constr ctx in
@@ -530,7 +518,7 @@ let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
let u_s = EInstance.kind sigma u in
let cl = Typeclasses.typeclass_univ_instance (k, u_s) in
let args = List.map of_constr args in
- let cl_context = List.map (Termops.map_rel_decl of_constr) (snd cl.cl_context) in
+ let cl_context = List.map (Termops.map_rel_decl of_constr) cl.cl_context in
let _, args =
List.fold_right (fun decl (args, args') ->
match decl with
diff --git a/vernac/comTactic.ml b/vernac/comTactic.ml
index 8a9a412362..2252d46e58 100644
--- a/vernac/comTactic.ml
+++ b/vernac/comTactic.ml
@@ -16,13 +16,13 @@ module DMap = Dyn.Map(struct type 'a t = 'a -> unit Proofview.tactic end)
let interp_map = ref DMap.empty
-type 'a tactic_interpreter = 'a Dyn.tag
-type interpretable = I : 'a tactic_interpreter * 'a -> interpretable
+type interpretable = I : 'a Dyn.tag * 'a -> interpretable
+type 'a tactic_interpreter = Interpreter of ('a -> interpretable)
let register_tactic_interpreter na f =
let t = Dyn.create na in
interp_map := DMap.add t f !interp_map;
- t
+ Interpreter (fun x -> I (t,x))
let interp_tac (I (tag,t)) =
let f = DMap.find tag !interp_map in
diff --git a/vernac/comTactic.mli b/vernac/comTactic.mli
index f1a75e1b6a..72e71d013a 100644
--- a/vernac/comTactic.mli
+++ b/vernac/comTactic.mli
@@ -9,10 +9,13 @@
(************************************************************************)
(** Tactic interpreters have to register their interpretation function *)
-type 'a tactic_interpreter
-type interpretable = I : 'a tactic_interpreter * 'a -> interpretable
+type interpretable
-(** ['a] should be marshallable if ever used with [par:] *)
+type 'a tactic_interpreter = private Interpreter of ('a -> interpretable)
+
+(** ['a] should be marshallable if ever used with [par:]. Must be
+ called no more than once per process with a particular string: make
+ sure to use partial application. *)
val register_tactic_interpreter :
string -> ('a -> unit Proofview.tactic) -> 'a tactic_interpreter
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 5274a6da3b..3a8ceb0e0f 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -162,7 +162,7 @@ let cache_constant ((sp,kn), obj) =
then Constant.make1 kn
else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(Libnames.basename sp) ++ str".")
in
- assert (Constant.equal kn' (Constant.make1 kn));
+ assert (Environ.QConstant.equal (Global.env ()) kn' (Constant.make1 kn));
Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn));
Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind
@@ -2206,26 +2206,60 @@ let warn_solve_errored =
; fnl ()
; str "This will become an error in the future" ])
-let solve_by_tac ?loc name evi t ~poly ~uctx =
- (* the status is dropped. *)
+let solve_by_tac prg obls i tac =
+ let obl = obls.(i) in
+ let obl = subst_deps_obl obls obl in
+ let tac = Option.(default !default_tactic (append tac obl.obl_tac)) in
+ let uctx = Internal.get_uctx prg in
+ let uctx = UState.update_sigma_univs uctx (Global.universes ()) in
+ let poly = Internal.get_poly prg in
+ let evi = evar_of_obligation obl in
+ (* the status of [build_by_tactic] is dropped. *)
try
let env = Global.env () in
let body, types, _univs, _, uctx =
- build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in
+ build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl tac in
Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body);
Some (body, types, uctx)
with
| Tacticals.FailError (_, s) as exn ->
let _ = Exninfo.capture exn in
+ let loc = fst obl.obl_location in
CErrors.user_err ?loc ~hdr:"solve_obligation" (Lazy.force s)
(* If the proof is open we absorb the error and leave the obligation open *)
| Proof_.OpenProof _ ->
None
| e when CErrors.noncritical e ->
let err = CErrors.print e in
+ let loc = fst obl.obl_location in
warn_solve_errored ?loc err;
None
+let solve_and_declare_by_tac prg obls i tac =
+ match solve_by_tac prg obls i tac with
+ | None -> None
+ | Some (t, ty, uctx) ->
+ let obl = obls.(i) in
+ let poly = Internal.get_poly prg in
+ let prg = ProgramDecl.Internal.set_uctx ~uctx prg in
+ let def, obl', _cst = declare_obligation prg obl ~body:t ~types:ty ~uctx in
+ obls.(i) <- obl';
+ if def && not poly then (
+ (* Declare the term constraints with the first obligation only *)
+ let uctx_global = UState.from_env (Global.env ()) in
+ let uctx = UState.merge_subst uctx_global (UState.subst uctx) in
+ Some (ProgramDecl.Internal.set_uctx ~uctx prg))
+ else Some prg
+
+let solve_obligation_by_tac prg obls i tac =
+ let obl = obls.(i) in
+ match obl.obl_body with
+ | Some _ -> None
+ | None ->
+ if List.is_empty (deps_remaining obls obl.obl_deps)
+ then solve_and_declare_by_tac prg obls i tac
+ else None
+
let get_unique_prog ~pm prg =
match State.get_unique_open_prog pm prg with
| Ok prg -> prg
@@ -2263,49 +2297,6 @@ let rec solve_obligation prg num tac =
let lemma = Option.cata (fun tac -> Proof.set_endline_tactic tac lemma) lemma tac in
lemma
-and obligation (user_num, name, typ) ~pm tac =
- let num = pred user_num in
- let prg = get_unique_prog ~pm name in
- let { obls; remaining } = Internal.get_obligations prg in
- if num >= 0 && num < Array.length obls then
- let obl = obls.(num) in
- match obl.obl_body with
- | None -> solve_obligation prg num tac
- | Some r -> Error.already_solved num
- else Error.unknown_obligation num
-
-and solve_obligation_by_tac prg obls i tac =
- let obl = obls.(i) in
- match obl.obl_body with
- | Some _ -> None
- | None ->
- if List.is_empty (deps_remaining obls obl.obl_deps) then
- let obl = subst_deps_obl obls obl in
- let tac =
- match tac with
- | Some t -> t
- | None ->
- match obl.obl_tac with
- | Some t -> t
- | None -> !default_tactic
- in
- let uctx = Internal.get_uctx prg 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
- | Some (t, ty, uctx) ->
- let prg = ProgramDecl.Internal.set_uctx ~uctx prg in
- let def, obl', _cst = declare_obligation prg obl ~body:t ~types:ty ~uctx in
- obls.(i) <- obl';
- if def && not poly then (
- (* Declare the term constraints with the first obligation only *)
- let uctx_global = UState.from_env (Global.env ()) in
- let uctx = UState.merge_subst uctx_global (UState.subst uctx) in
- Some (ProgramDecl.Internal.set_uctx ~uctx prg))
- else Some prg
- else None
-
and solve_prg_obligations ~pm prg ?oblset tac =
let { obls; remaining } = Internal.get_obligations prg in
let rem = ref remaining in
@@ -2332,15 +2323,21 @@ and solve_prg_obligations ~pm prg ?oblset tac =
in
update_obls ~pm prg obls' !rem
-and solve_obligations ~pm n tac =
+and auto_solve_obligations ~pm n ?oblset tac : State.t * progress =
+ Flags.if_verbose Feedback.msg_info
+ (str "Solving obligations automatically...");
+ let prg = get_unique_prog ~pm n in
+ solve_prg_obligations ~pm prg ?oblset tac
+
+let solve_obligations ~pm n tac =
let prg = get_unique_prog ~pm n in
solve_prg_obligations ~pm prg tac
-and solve_all_obligations ~pm tac =
+let solve_all_obligations ~pm tac =
State.fold pm ~init:pm ~f:(fun k v pm ->
solve_prg_obligations ~pm v tac |> fst)
-and try_solve_obligation ~pm n prg tac =
+let try_solve_obligation ~pm n prg tac =
let prg = get_unique_prog ~pm prg in
let {obls; remaining} = Internal.get_obligations prg in
let obls' = Array.copy obls in
@@ -2350,14 +2347,19 @@ and try_solve_obligation ~pm n prg tac =
pm
| None -> pm
-and try_solve_obligations ~pm n tac =
+let try_solve_obligations ~pm n tac =
solve_obligations ~pm n tac |> fst
-and auto_solve_obligations ~pm n ?oblset tac : State.t * progress =
- Flags.if_verbose Feedback.msg_info
- (str "Solving obligations automatically...");
- let prg = get_unique_prog ~pm n in
- solve_prg_obligations ~pm prg ?oblset tac
+let obligation (user_num, name, typ) ~pm tac =
+ let num = pred user_num in
+ let prg = get_unique_prog ~pm name in
+ let { obls; remaining } = Internal.get_obligations prg in
+ if num >= 0 && num < Array.length obls then
+ let obl = obls.(num) in
+ match obl.obl_body with
+ | None -> solve_obligation prg num tac
+ | Some r -> Error.already_solved num
+ else Error.unknown_obligation num
let show_single_obligation i n obls x =
let x = subst_deps_obl obls x in
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 5f7eb78a40..bef9e29ac2 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -656,7 +656,7 @@ let explain_evar_not_found env sigma id =
let explain_wrong_case_info env (ind,u) ci =
let pi = pr_inductive env ind in
- if eq_ind ci.ci_ind ind then
+ if Ind.CanOrd.equal ci.ci_ind ind then
str "Pattern-matching expression on an object of inductive type" ++
spc () ++ pi ++ spc () ++ str "has invalid information."
else
@@ -1232,7 +1232,7 @@ let error_not_allowed_dependent_analysis env isrec i =
pr_inductive env i ++ str "."
let error_not_mutual_in_scheme env ind ind' =
- if eq_ind ind ind' then
+ if Ind.CanOrd.equal ind ind' then
str "The inductive type " ++ pr_inductive env ind ++
str " occurs twice."
else
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 356ccef06b..de72a30f18 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -405,7 +405,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
let get_common_underlying_mutual_inductive env = function
| [] -> assert false
| (id,(mind,i as ind))::l as all ->
- match List.filter (fun (_,(mind',_)) -> not (MutInd.equal mind mind')) l with
+ match List.filter (fun (_,(mind',_)) -> not (Environ.QMutInd.equal env mind mind')) l with
| (_,ind')::_ ->
raise (RecursionSchemeError (env, NotMutualInScheme (ind,ind')))
| [] ->
diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml
index 534c358a3f..af72c01758 100644
--- a/vernac/recLemmas.ml
+++ b/vernac/recLemmas.ml
@@ -44,7 +44,7 @@ let find_mutually_recursive_statements sigma thms =
[] in
ind_hyps,ind_ccl) thms in
let inds_hyps,ind_ccls = List.split inds in
- let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> Names.MutInd.equal kn kn' in
+ let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> Environ.QMutInd.equal (Global.env ()) kn kn' in
(* Check if all conclusions are coinductive in the same type *)
(* (degenerated cartesian product since there is at most one coind ccl) *)
let same_indccl =
@@ -70,7 +70,7 @@ let find_mutually_recursive_statements sigma thms =
| [], _::_ ->
let () = match same_indccl with
| ind :: _ ->
- if List.distinct_f Names.ind_ord (List.map pi1 ind)
+ if List.distinct_f Names.Ind.CanOrd.compare (List.map pi1 ind)
then
Flags.if_verbose Feedback.msg_info
(Pp.strbrk
diff --git a/vernac/record.ml b/vernac/record.ml
index a4bf9893d9..acc97f61c1 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -582,26 +582,17 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
in
List.map map inds
in
- let ctx_context =
- let env = Global.env () in
- let sigma = Evd.from_env env in
- List.map (fun decl ->
- match Typeclasses.class_of_constr env sigma (EConstr.of_constr (RelDecl.get_type decl)) with
- | Some (_, ((cl,_), _)) -> Some cl.cl_impl
- | None -> None)
- params, params
- in
- let univs, ctx_context, fields =
+ let univs, params, fields =
match univs with
| Polymorphic_entry (nas, univs) ->
let usubst, auctx = Univ.abstract_universes nas univs in
let usubst = Univ.make_instance_subst usubst in
let map c = Vars.subst_univs_level_constr usubst c in
let fields = Context.Rel.map map fields in
- let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in
- auctx, ctx_context, fields
+ let params = Context.Rel.map map params in
+ auctx, params, fields
| Monomorphic_entry _ ->
- Univ.AUContext.empty, ctx_context, fields
+ Univ.AUContext.empty, params, fields
in
let map (impl, projs) =
let k =
@@ -609,7 +600,7 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
cl_impl = impl;
cl_strict = !typeclasses_strict;
cl_unique = !typeclasses_unique;
- cl_context = ctx_context;
+ cl_context = params;
cl_props = fields;
cl_projs = projs }
in
@@ -629,7 +620,7 @@ let add_constant_class env sigma cst =
let tc =
{ cl_univs = univs;
cl_impl = GlobRef.ConstRef cst;
- cl_context = (List.map (const None) ctx, ctx);
+ cl_context = ctx;
cl_props = [LocalAssum (make_annot Anonymous r, t)];
cl_projs = [];
cl_strict = !typeclasses_strict;
@@ -651,7 +642,7 @@ let add_inductive_class env sigma ind =
let r = Inductive.relevance_of_inductive env ind in
{ cl_univs = univs;
cl_impl = GlobRef.IndRef ind;
- cl_context = List.map (const None) ctx, ctx;
+ cl_context = ctx;
cl_props = [LocalAssum (make_annot Anonymous r, ty)];
cl_projs = [];
cl_strict = !typeclasses_strict;
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 01:40:48 +0000