aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/derive/derive.ml2
-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/indfun.ml2
-rw-r--r--plugins/funind/recdef.ml6
-rw-r--r--plugins/ltac/extratactics.mlg7
-rw-r--r--plugins/ltac/g_auto.mlg3
-rw-r--r--plugins/ltac/rewrite.ml4
-rw-r--r--plugins/ltac/tacinterp.ml80
-rw-r--r--plugins/setoid_ring/newring.ml2
-rw-r--r--plugins/ssr/ssrast.mli3
-rw-r--r--plugins/ssr/ssrcommon.ml4
-rw-r--r--plugins/ssr/ssrparser.mlg6
-rw-r--r--plugins/ssr/ssrparser.mli53
-rw-r--r--plugins/ssr/ssrvernac.mlg20
16 files changed, 195 insertions, 68 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 6f9384941b..d06a241969 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -40,7 +40,7 @@ let start_deriving f suchthat lemma =
let f_type = EConstr.Unsafe.to_constr f_type in
let ef = EConstr.Unsafe.to_constr ef in
let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in
- let sigma, suchthat = Constrintern.interp_type_evars env' sigma suchthat in
+ let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in
TCons ( env' , sigma , suchthat , (fun sigma _ ->
TNil sigma))))))
in
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/indfun.ml b/plugins/funind/indfun.ml
index d9b0330e2b..42dc66dcf4 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -166,7 +166,7 @@ let build_newrecursive
let arityc = Constrexpr_ops.mkCProdN bl arityc in
let arity,ctx = Constrintern.interp_type env0 sigma arityc in
let evd = Evd.from_env env0 in
- let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in
+ let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in
let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in
let open Context.Named.Declaration in
(EConstr.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls))
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1b5286dce4..a8517e9ab1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1518,10 +1518,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let open CVars in
let env = Global.env() in
let evd = Evd.from_env env in
- let evd, function_type = interp_type_evars env evd type_of_f in
+ let evd, function_type = interp_type_evars ~program_mode:false env evd type_of_f in
let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in
(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
- let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in
+ let evd, ty = interp_type_evars ~program_mode:false env evd ~impls:rec_impls eq in
let evd = Evd.minimize_universes evd in
let equation_lemma_type = Reductionops.nf_betaiotazeta env evd (Evarutil.nf_evar evd ty) in
let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in
@@ -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/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 47f593ff3e..ffd8b71e5d 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -50,7 +50,8 @@ let with_delayed_uconstr ist c tac =
Pretyping.use_typeclasses = false;
solve_unification_constraints = true;
fail_evar = false;
- expand_evars = true
+ expand_evars = true;
+ program_mode = false;
} in
let c = Tacinterp.type_uconstr ~flags ist c in
Tacticals.New.tclDELAYEDWITHHOLES false c tac
@@ -344,7 +345,9 @@ let constr_flags () = {
Pretyping.use_typeclasses = true;
Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
Pretyping.fail_evar = false;
- Pretyping.expand_evars = true }
+ Pretyping.expand_evars = true;
+ Pretyping.program_mode = false;
+}
let refine_tac ist simple with_classes c =
Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 7be8f67616..663537f3e8 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -56,7 +56,8 @@ let eval_uconstrs ist cs =
Pretyping.use_typeclasses = false;
solve_unification_constraints = true;
fail_evar = false;
- expand_evars = true
+ expand_evars = true;
+ program_mode = false;
} in
let map c env sigma = c env sigma in
List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs
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 3e7479903a..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
@@ -530,7 +542,15 @@ let interp_gen kind ist pattern_mode flags env sigma c =
invariant that running the tactic returned by push_trace does
not modify sigma. *)
let (_, dummy_proofview) = Proofview.init sigma [] in
- let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in
+
+ (* Again this is called at times with no open proof! *)
+ let name, poly =
+ try
+ let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in
+ name, poly
+ with | Proof_global.NoCurrentProof -> Id.of_string "tacinterp", false
+ in
+ let (trace,_,_,_) = Proofview.apply ~name ~poly env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in
let (evd,c) =
catch_error trace (understand_ltac flags env sigma vars kind) term
in
@@ -544,7 +564,9 @@ let constr_flags () = {
use_typeclasses = true;
solve_unification_constraints = true;
fail_evar = true;
- expand_evars = true }
+ expand_evars = true;
+ program_mode = false;
+}
(* Interprets a constr; expects evars to be solved *)
let interp_constr_gen kind ist env sigma c =
@@ -558,19 +580,25 @@ let open_constr_use_classes_flags () = {
use_typeclasses = true;
solve_unification_constraints = true;
fail_evar = false;
- expand_evars = true }
+ expand_evars = true;
+ program_mode = false;
+}
let open_constr_no_classes_flags () = {
use_typeclasses = false;
solve_unification_constraints = true;
fail_evar = false;
- expand_evars = true }
+ expand_evars = true;
+ program_mode = false;
+}
let pure_open_constr_flags = {
use_typeclasses = false;
solve_unification_constraints = true;
fail_evar = false;
- expand_evars = false }
+ expand_evars = false;
+ program_mode = false;
+}
(* Interprets an open constr *)
let interp_open_constr ?(expected_type=WithoutTypeConstraint) ?(flags=open_constr_no_classes_flags ()) ist env sigma c =
@@ -1247,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;
@@ -1407,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) ->
@@ -1493,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 ->
@@ -2033,7 +2061,16 @@ let _ =
let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
let ist = { lfun = lfun; extra; } in
let tac = interp_tactic ist tac in
- let name, poly = Id.of_string "ltac_sub", false in
+ (* XXX: This depends on the global state which is bad; the hooking
+ mechanism should be modified. *)
+ let name, poly =
+ try
+ let (_, poly, _) = Proof_global.get_current_persistence () in
+ let name = Proof_global.get_current_proof_name () in
+ name, poly
+ with | Proof_global.NoCurrentProof ->
+ Id.of_string "ltac_gen", false
+ in
let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in
(EConstr.of_constr c, sigma)
in
@@ -2051,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))
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 9ce9250a43..0897d3b45b 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -137,6 +137,9 @@ type 'tac ssrhint = bool * 'tac option list
type 'tac fwdbinders =
bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint))
+type 'tac ffwbinders =
+ (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint))
+
type clause =
(ssrclear * ((ssrhyp_or_id * string) *
Ssrmatching_plugin.Ssrmatching.cpattern option) option)
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index c3b9bde9b8..0961edb6cb 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -243,7 +243,9 @@ let interp_refine ist gl rc =
Pretyping.use_typeclasses = true;
solve_unification_constraints = true;
fail_evar = false;
- expand_evars = true }
+ expand_evars = true;
+ program_mode = false;
+ }
in
let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in
(* ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *)
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 3fb21e5ef6..2a2cd73df2 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -591,10 +591,8 @@ END
GRAMMAR EXTEND Gram
GLOBAL: ssrfwdview;
ssrfwdview: [
- [ test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr ->
- { [mk_ast_closure_term `None c] }
- | test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr; w = ssrfwdview ->
- { (mk_ast_closure_term `None c) :: w } ]];
+ [ test_not_ssrslashnum; "/"; c = ast_closure_term -> { [c] }
+ | test_not_ssrslashnum; "/"; c = ast_closure_term; w = ssrfwdview -> { c :: w } ]];
END
(* ipats *)
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index a2cbd3c9c8..7844050272 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -32,6 +32,19 @@ type ssrfwdview = ast_closure_term list
type ssreqid = ssripat option
type ssrarg = ssrfwdview * (ssreqid * (cpattern ssragens * ssripats))
+val wit_ssrseqdir : ssrdir Genarg.uniform_genarg_type
+val wit_ssrseqarg : (Tacexpr.raw_tactic_expr ssrseqarg, Tacexpr.glob_tactic_expr ssrseqarg, Geninterp.Val.t ssrseqarg) Genarg.genarg_type
+
+val wit_ssrintrosarg :
+ (Tacexpr.raw_tactic_expr * ssripats,
+ Tacexpr.glob_tactic_expr * ssripats,
+ Geninterp.Val.t * ssripats) Genarg.genarg_type
+
+val wit_ssrsufffwd :
+ (Tacexpr.raw_tactic_expr ffwbinders,
+ Tacexpr.glob_tactic_expr ffwbinders,
+ Geninterp.Val.t ffwbinders) Genarg.genarg_type
+
val wit_ssripatrep : ssripat Genarg.uniform_genarg_type
val wit_ssrarg : ssrarg Genarg.uniform_genarg_type
val wit_ssrrwargs : ssrrwarg list Genarg.uniform_genarg_type
@@ -47,3 +60,43 @@ val wit_ssrhintarg :
(Tacexpr.raw_tactic_expr ssrhint,
Tacexpr.glob_tactic_expr ssrhint,
Tacinterp.Value.t ssrhint) Genarg.genarg_type
+
+val wit_ssrexactarg : ssrapplyarg Genarg.uniform_genarg_type
+val wit_ssrcongrarg : ((int * ssrterm) * cpattern ssragens) Genarg.uniform_genarg_type
+val wit_ssrfwdid : Names.Id.t Genarg.uniform_genarg_type
+
+val wit_ssrsetfwd :
+ ((ssrfwdfmt * (cpattern * ast_closure_term option)) * ssrdocc) Genarg.uniform_genarg_type
+
+val wit_ssrdoarg :
+ (Tacexpr.raw_tactic_expr ssrdoarg,
+ Tacexpr.glob_tactic_expr ssrdoarg,
+ Tacinterp.Value.t ssrdoarg) Genarg.genarg_type
+
+val wit_ssrhint :
+ (Tacexpr.raw_tactic_expr ssrhint,
+ Tacexpr.glob_tactic_expr ssrhint,
+ Tacinterp.Value.t ssrhint) Genarg.genarg_type
+
+val wit_ssrhpats : ssrhpats Genarg.uniform_genarg_type
+val wit_ssrhpats_nobs : ssrhpats Genarg.uniform_genarg_type
+val wit_ssrhpats_wtransp : ssrhpats_wtransp Genarg.uniform_genarg_type
+
+val wit_ssrposefwd : (ssrfwdfmt * ast_closure_term) Genarg.uniform_genarg_type
+
+val wit_ssrrpat : ssripat Genarg.uniform_genarg_type
+val wit_ssrterm : ssrterm Genarg.uniform_genarg_type
+val wit_ssrunlockarg : (ssrocc * ssrterm) Genarg.uniform_genarg_type
+val wit_ssrunlockargs : (ssrocc * ssrterm) list Genarg.uniform_genarg_type
+
+val wit_ssrwgen : clause Genarg.uniform_genarg_type
+val wit_ssrwlogfwd : (clause list * (ssrfwdfmt * ast_closure_term)) Genarg.uniform_genarg_type
+
+val wit_ssrfixfwd : (Names.Id.t * (ssrfwdfmt * ast_closure_term)) Genarg.uniform_genarg_type
+val wit_ssrfwd : (ssrfwdfmt * ast_closure_term) Genarg.uniform_genarg_type
+val wit_ssrfwdfmt : ssrfwdfmt Genarg.uniform_genarg_type
+
+val wit_ssrcpat : ssripat Genarg.uniform_genarg_type
+val wit_ssrdgens : cpattern ssragens Genarg.uniform_genarg_type
+val wit_ssrdgens_tl : cpattern ssragens Genarg.uniform_genarg_type
+val wit_ssrdir : ssrdir Genarg.uniform_genarg_type
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 191a4e9a20..d083d34b52 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -596,26 +596,6 @@ VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF
Ssrview.AdaptorDb.declare k hints }
END
-(** Canonical Structure alias *)
-
-GRAMMAR EXTEND Gram
- GLOBAL: gallina_ext;
-
- gallina_ext:
- (* Canonical structure *)
- [[ IDENT "Canonical"; qid = Constr.global ->
- { Vernacexpr.VernacCanonical (CAst.make @@ AN qid) }
- | IDENT "Canonical"; ntn = Prim.by_notation ->
- { Vernacexpr.VernacCanonical (CAst.make @@ ByNotation ntn) }
- | IDENT "Canonical"; qid = Constr.global;
- d = G_vernac.def_body ->
- { let s = coerce_reference_to_id qid in
- Vernacexpr.VernacDefinition
- ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure),
- ((CAst.make (Name s)),None), d) }
- ]];
-END
-
(** Keyword compatibility fixes. *)
(* Coq v8.1 notation uses "by" and "of" quasi-keywords, i.e., reserved *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 16:03:27 +0000