aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/extraction.ml59
-rw-r--r--plugins/funind/functional_principles_types.ml2
-rw-r--r--plugins/funind/glob_term_to_relation.ml10
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--plugins/ltac/rewrite.ml4
-rw-r--r--plugins/ltac/tacinterp.ml43
-rw-r--r--plugins/setoid_ring/newring.ml2
7 files changed, 92 insertions, 30 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index c15486ea10..204f889f90 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1032,6 +1032,55 @@ let extract_fixpoint env sg vkn (fi,ti,ci) =
current_fixpoints := [];
Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types)
+(** Because of automatic unboxing the easy way [mk_def c] on the
+ constant body of primitive projections doesn't work. We pretend
+ that they are implemented by matches until someone figures out how
+ to clean it up (test with #4710 when working on this). *)
+let fake_match_projection env p =
+ let ind = Projection.Repr.inductive p in
+ let proj_arg = Projection.Repr.arg p in
+ let mib, mip = Inductive.lookup_mind_specif env ind in
+ let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
+ let indu = mkIndU (ind,u) in
+ let ctx, paramslet =
+ let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in
+ let rctx, _ = decompose_prod_assum (Vars.substl subst mip.mind_nf_lc.(0)) in
+ List.chop mip.mind_consnrealdecls.(0) rctx
+ in
+ let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
+ let ci = {
+ ci_ind = ind;
+ ci_npar = mib.mind_nparams;
+ ci_cstr_ndecls = mip.mind_consnrealdecls;
+ ci_cstr_nargs = mip.mind_consnrealargs;
+ ci_pp_info;
+ }
+ in
+ let x = match mib.mind_record with
+ | NotRecord | FakeRecord -> assert false
+ | PrimRecord info -> Name (pi1 info.(snd ind))
+ in
+ let indty = mkApp (indu, Context.Rel.to_extended_vect mkRel 0 paramslet) in
+ let rec fold arg j subst = function
+ | [] -> assert false
+ | LocalAssum (na,ty) :: rem ->
+ let ty = Vars.substl subst (liftn 1 j ty) in
+ if arg != proj_arg then
+ let lab = match na with Name id -> Label.of_id id | Anonymous -> assert false in
+ let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in
+ fold (arg+1) (j+1) (mkProj (Projection.make kn false, mkRel 1)::subst) rem
+ else
+ let p = mkLambda (x, lift 1 indty, liftn 1 2 ty) in
+ let branch = lift 1 (it_mkLambda_or_LetIn (mkRel (List.length ctx - (j-1))) ctx) in
+ let body = mkCase (ci, p, mkRel 1, [|branch|]) in
+ it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt
+ | LocalDef (_,c,t) :: rem ->
+ let c = liftn 1 j c in
+ let c1 = Vars.substl subst c in
+ fold arg (j+1) (c1::subst) rem
+ in
+ fold 0 1 [] (List.rev ctx)
+
let extract_constant env kn cb =
let sg = Evd.from_env env in
let r = ConstRef kn in
@@ -1069,10 +1118,7 @@ let extract_constant env kn cb =
(match Recordops.find_primitive_projection kn with
| None -> mk_typ (get_body c)
| Some p ->
- let p = Projection.make p false in
- let ind = Projection.inductive p in
- let bodies = Inductiveops.legacy_match_projection env ind in
- let body = bodies.(Projection.arg p) in
+ let body = fake_match_projection env p in
mk_typ (EConstr.of_constr body))
| OpaqueDef c ->
add_opaque r;
@@ -1085,10 +1131,7 @@ let extract_constant env kn cb =
(match Recordops.find_primitive_projection kn with
| None -> mk_def (get_body c)
| Some p ->
- let p = Projection.make p false in
- let ind = Projection.inductive p in
- let bodies = Inductiveops.legacy_match_projection env ind in
- let body = bodies.(Projection.arg p) in
+ let body = fake_match_projection env p in
mk_def (EConstr.of_constr body))
| OpaqueDef c ->
add_opaque r;
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 12b68e208c..25a7675113 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -364,7 +364,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
- let univs = Evd.const_univ_entry ~poly:false evd' in
+ let univs = Evd.univ_entry ~poly:false evd' in
let ce = Declare.definition_entry ~univs value in
ignore(
Declare.declare_constant
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 02964d7ba5..ba0a3bbb5c 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -321,12 +321,10 @@ let build_constructors_of_type ind' argl =
construct
in
let argl =
- if List.is_empty argl
- then
- Array.to_list
- (Array.init (cst_narg - npar) (fun _ -> mkGHole ())
- )
- else argl
+ if List.is_empty argl then
+ List.make cst_narg (mkGHole ())
+ else
+ List.make npar (mkGHole ()) @ argl
in
let pat_as_term =
mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 0c97f9f373..a8517e9ab1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1547,7 +1547,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let functional_id = add_suffix function_name "_F" in
let term_id = add_suffix function_name "_terminate" in
let functional_ref =
- let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in
+ let univs = Evd.univ_entry ~poly:false evd in
declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res
in
(* Refresh the global universes, now including those of _F *)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2055b25ff4..7da4464e59 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1889,7 +1889,7 @@ let declare_projection n instance_id r =
in it_mkProd_or_LetIn ccl ctx
in
let typ = it_mkProd_or_LetIn typ ctx in
- let univs = Evd.const_univ_entry ~poly sigma in
+ let univs = Evd.univ_entry ~poly sigma in
let typ = EConstr.to_constr sigma typ in
let term = EConstr.to_constr sigma term in
let cst =
@@ -1975,7 +1975,7 @@ let add_morphism_infer atts m n =
let evd = Evd.from_env env in
let uctx, instance = build_morphism_signature env evd m in
if Lib.is_modtype () then
- let uctx = UState.const_univ_entry ~poly:atts.polymorphic uctx in
+ let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
(Entries.ParameterEntry
(None,(instance,uctx),None),
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 62906303a4..30f716d764 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -117,9 +117,14 @@ let combine_appl appl1 appl2 =
let of_tacvalue v = in_gen (topwit wit_tacvalue) v
let to_tacvalue v = out_gen (topwit wit_tacvalue) v
+let log_trace = ref false
+
+let is_traced () =
+ !log_trace || !Flags.profile_ltac
+
(** More naming applications *)
let name_vfun appl vle =
- if has_type vle (topwit wit_tacvalue) then
+ if is_traced () && has_type vle (topwit wit_tacvalue) then
match to_tacvalue vle with
| VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t))
| _ -> vle
@@ -137,9 +142,11 @@ type interp_sign = Geninterp.interp_sign = {
lfun : value Id.Map.t;
extra : TacStore.t }
-let extract_trace ist = match TacStore.get ist.extra f_trace with
-| None -> []
-| Some l -> l
+let extract_trace ist =
+ if is_traced () then match TacStore.get ist.extra f_trace with
+ | None -> []
+ | Some l -> l
+ else []
let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
@@ -161,8 +168,11 @@ let catch_error call_trace f x =
let e = CErrors.push e in
catching_error call_trace iraise e
+let wrap_error tac k =
+ if is_traced () then Proofview.tclORELSE tac k else tac
+
let catch_error_tac call_trace tac =
- Proofview.tclORELSE
+ wrap_error
tac
(catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
@@ -203,9 +213,11 @@ let constr_of_id env id =
(** Generic arguments : table of interpretation functions *)
(* Some of the code further down depends on the fact that push_trace does not modify sigma (the evar map) *)
-let push_trace call ist = match TacStore.get ist.extra f_trace with
-| None -> Proofview.tclUNIT [call]
-| Some trace -> Proofview.tclUNIT (call :: trace)
+let push_trace call ist =
+ if is_traced () then match TacStore.get ist.extra f_trace with
+ | None -> Proofview.tclUNIT [call]
+ | Some trace -> Proofview.tclUNIT (call :: trace)
+ else Proofview.tclUNIT []
let propagate_trace ist loc id v =
if has_type v (topwit wit_tacvalue) then
@@ -1263,7 +1275,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
let fold accu (id, v) = Id.Map.add id v accu in
let newlfun = List.fold_left fold olfun extfun in
if List.is_empty lvar then
- begin Proofview.tclORELSE
+ begin wrap_error
begin
let ist = {
lfun = newlfun;
@@ -1423,7 +1435,7 @@ and interp_match_successes lz ist s =
(* Interprets the Match expressions *)
and interp_match ist lz constr lmr =
let (>>=) = Ftactic.bind in
- begin Proofview.tclORELSE
+ begin wrap_error
(interp_ltac_constr ist constr)
begin function
| (e, info) ->
@@ -1509,7 +1521,7 @@ and interp_genarg_var_list ist x =
(* Interprets tactic expressions : returns a "constr" *)
and interp_ltac_constr ist e : EConstr.t Ftactic.t =
let (>>=) = Ftactic.bind in
- begin Proofview.tclORELSE
+ begin wrap_error
(val_interp ist e)
begin function (err, info) -> match err with
| Not_found ->
@@ -2076,4 +2088,13 @@ let () =
optread = (fun () -> get_debug () != Tactic_debug.DebugOff);
optwrite = vernac_debug }
+let () =
+ let open Goptions in
+ declare_bool_option
+ { optdepr = false;
+ optname = "Ltac Backtrace";
+ optkey = ["Ltac"; "Backtrace"];
+ optread = (fun () -> !log_trace);
+ optwrite = (fun b -> log_trace := b) }
+
let () = Hook.set Vernacentries.interp_redexp_hook interp_redexp
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 65201d922f..3f69701bd3 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -153,7 +153,7 @@ let decl_constant na univs c =
let open Constr in
let vars = CVars.universes_of_constr c in
let univs = UState.restrict_universe_context univs vars in
- let univs = Monomorphic_const_entry univs in
+ let univs = Monomorphic_entry univs in
mkConst(declare_constant (Id.of_string na)
(DefinitionEntry (definition_entry ~opaque:true ~univs c),
IsProof Lemma))
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 17:02:24 +0000