aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/gen_principle.ml10
-rw-r--r--plugins/funind/recdef.ml6
-rw-r--r--plugins/ltac/g_ltac.mlg2
-rw-r--r--plugins/ltac/rewrite.ml12
-rw-r--r--plugins/ltac/tacentries.ml105
-rw-r--r--plugins/ltac/tacentries.mli19
-rw-r--r--plugins/ltac/tacinterp.ml14
-rw-r--r--plugins/ltac/tacinterp.mli1
-rw-r--r--plugins/micromega/coq_micromega.ml380
-rw-r--r--plugins/ssr/ssrparser.mlg4
10 files changed, 277 insertions, 276 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index c53dcc7edd..608155eb71 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -218,7 +218,7 @@ let build_functional_principle (sigma : Evd.evar_map) old_princ_type sorts funs
Declare.build_by_tactic env ~uctx ~poly:false ~typ ftac
in
(* uctx was ignored before *)
- let hook = DeclareDef.Hook.make (hook new_principle_type) in
+ let hook = Declare.Hook.make (hook new_principle_type) in
(body, typ, univs, hook, sigma)
let change_property_sort evd toSort princ princName =
@@ -318,8 +318,8 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts
let uctx = Evd.evar_universe_context sigma in
let entry = Declare.definition_entry ~univs ?types body in
let (_ : Names.GlobRef.t) =
- DeclareDef.declare_entry ~name:new_princ_name ~hook
- ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+ Declare.declare_entry ~name:new_princ_name ~hook
+ ~scope:(Declare.Global Declare.ImportDefaultBehavior)
~kind:Decls.(IsProof Theorem)
~impargs:[] ~uctx entry
in
@@ -400,7 +400,7 @@ let register_struct is_rec fixpoint_exprl =
Pp.(str "Body of Function must be given")
in
ComDefinition.do_definition ~name:fname.CAst.v ~poly:false
- ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+ ~scope:(Declare.Global Declare.ImportDefaultBehavior)
~kind:Decls.Definition univs binders None body (Some rtype);
let evd, rev_pconstants =
List.fold_left
@@ -419,7 +419,7 @@ let register_struct is_rec fixpoint_exprl =
(None, evd, List.rev rev_pconstants)
| _ ->
ComFixpoint.do_fixpoint
- ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false
+ ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~poly:false
fixpoint_exprl;
let evd, rev_pconstants =
List.fold_left
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ffb9a7e69b..5c82ed38bb 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1483,7 +1483,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None
in
- let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in
+ let info = Lemmas.Info.make ~hook:(Declare.Hook.make hook) () in
let lemma =
Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info sigma gls_type
in
@@ -1721,7 +1721,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
let tcc_lemma_name = add_suffix function_name "_tcc" in
let tcc_lemma_constr = ref Undefined in
(* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
- let hook {DeclareDef.Hook.S.uctx; _} =
+ let hook {Declare.Hook.S.uctx; _} =
let term_ref = Nametab.locate (qualid_of_ident term_id) in
let f_ref =
declare_f function_name Decls.(IsProof Lemma) arg_types term_ref
@@ -1767,5 +1767,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
functional_ref
(EConstr.of_constr rec_arg_type)
relation rec_arg_num term_id using_lemmas (List.length res_vars) evd
- (DeclareDef.Hook.make hook))
+ (Declare.Hook.make hook))
()
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 5baa23b3e9..aef5f645f4 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -342,7 +342,7 @@ GRAMMAR EXTEND Gram
hint:
[ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
tac = Pltac.tactic ->
- { ComHints.HintsExtern (n,c, in_tac tac) } ] ]
+ { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ]
;
operconstr: LEVEL "0"
[ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3834b21a14..3b8fb48eb0 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1894,10 +1894,10 @@ let declare_projection name instance_id r =
in it_mkProd_or_LetIn ccl ctx
in
let types = Some (it_mkProd_or_LetIn typ ctx) in
- let kind, opaque, scope = Decls.(IsDefinition Definition), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+ let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in
let impargs, udecl = [], UState.default_univ_decl in
let _r : GlobRef.t =
- DeclareDef.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
+ Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
in ()
let build_morphism_signature env sigma m =
@@ -1961,10 +1961,10 @@ let add_morphism_as_parameter atts m n : unit =
let env = Global.env () in
let evd = Evd.from_env env in
let poly = atts.polymorphic in
- let kind, opaque, scope = Decls.(IsAssumption Logical), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+ let kind, opaque, scope = Decls.(IsAssumption Logical), false, Declare.Global Declare.ImportDefaultBehavior in
let impargs, udecl = [], UState.default_univ_decl in
let evd, types = build_morphism_signature env evd m in
- let evd, pe = DeclareDef.prepare_parameter ~poly ~udecl ~types evd in
+ let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in
let cst = Declare.declare_constant ~name:instance_id ~kind (Declare.ParameterEntry pe) in
let cst = GlobRef.ConstRef cst in
Classes.add_instance
@@ -1981,7 +1981,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
let poly = atts.polymorphic in
let kind = Decls.(IsDefinition Instance) in
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
- let hook { DeclareDef.Hook.S.dref; _ } = dref |> function
+ let hook { Declare.Hook.S.dref; _ } = dref |> function
| GlobRef.ConstRef cst ->
Classes.add_instance (Classes.mk_instance
(PropGlobal.proper_class env evd) Hints.empty_hint_info
@@ -1989,7 +1989,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
declare_projection n instance_id (GlobRef.ConstRef cst)
| _ -> assert false
in
- let hook = DeclareDef.Hook.make hook in
+ let hook = Declare.Hook.make hook in
let info = Lemmas.Info.make ~hook ~kind () in
Flags.silently
(fun () ->
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 9910796d9c..e6c59f446d 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -683,6 +683,111 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign =
Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign);
Mltop.declare_cache_obj obj plugin_name
+type (_, 'a) ml_ty_sig =
+| MLTyNil : ('a, 'a) ml_ty_sig
+| MLTyArg : ('r, 'a) ml_ty_sig -> (Geninterp.Val.t -> 'r, 'a) ml_ty_sig
+
+let rec ml_sig_len : type r a. (r, a) ml_ty_sig -> int = function
+| MLTyNil -> 0
+| MLTyArg sign -> 1 + ml_sig_len sign
+
+let rec cast_ml : type r a. (r, a) ml_ty_sig -> r -> Geninterp.Val.t list -> a =
+ fun sign f ->
+ match sign with
+ | MLTyNil ->
+ begin function
+ | [] -> f
+ | _ :: _ -> CErrors.anomaly (str "Arity mismatch")
+ end
+ | MLTyArg sign ->
+ function
+ | [] -> CErrors.anomaly (str "Arity mismatch")
+ | arg :: args -> cast_ml sign (f arg) args
+
+let ml_tactic_extend ~plugin ~name ~local ?deprecation sign tac =
+ let open Tacexpr in
+ let tac args _ = cast_ml sign tac args in
+ let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in
+ let ml = { mltac_name = ml_tactic_name; mltac_index = 0 } in
+ let len = ml_sig_len sign in
+ let args = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in
+ let vars = List.map (fun id -> Name id) args in
+ let args = List.map (fun id -> Reference (Locus.ArgVar (CAst.make id))) args in
+ let body = Tacexpr.TacFun (vars, Tacexpr.TacML (CAst.make (ml, args))) in
+ let id = Names.Id.of_string name in
+ let obj () = Tacenv.register_ltac true local id body ?deprecation in
+ let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in
+ Mltop.declare_cache_obj obj plugin
+
+module MLName =
+struct
+ open Tacexpr
+ type t = ml_tactic_name
+ let compare tac1 tac2 =
+ let c = String.compare tac1.mltac_tactic tac2.mltac_tactic in
+ if c = 0 then String.compare tac1.mltac_plugin tac2.mltac_plugin
+ else c
+end
+
+module MLTacMap = Map.Make(MLName)
+
+let ml_table : (Geninterp.Val.t list -> Geninterp.Val.t Ftactic.t) MLTacMap.t ref = ref MLTacMap.empty
+
+type ml_ltac_val = {
+ tacval_tac : Tacexpr.ml_tactic_name;
+ tacval_var : Id.t list;
+}
+
+let in_tacval =
+(* This is a hack to emulate value-returning ML-implemented tactics in Ltac.
+ We use a dummy generic argument to work around the limitations of the Ltac
+ runtime. Indeed, the TacML node needs to return unit values, since it is
+ considered a "tactic" in the runtime. Changing it to allow arbitrary values
+ would require to toggle this status, and thus to make it a "value" node.
+ This would in turn create too much backwards incompatibility. Instead, we
+ piggy back on the TacGeneric node, which by construction is used to return
+ values.
+
+ The trick is to represent a n-ary application of a ML function as a generic
+ argument. We store in the node the name of the tactic and its arity, while
+ giving canonical names to the bound variables of the closure. This trick is
+ already performed in several external developments for specific calls, we
+ make it here generic. The argument should not be used for other purposes, so
+ we only export the registering functions.
+ *)
+ let wit : (Empty.t, ml_ltac_val, Geninterp.Val.t) Genarg.genarg_type =
+ Genarg.create_arg "ltac:val"
+ in
+ (* No need to internalize this ever *)
+ let intern_fun _ e = Empty.abort e in
+ let subst_fun s v = v in
+ let () = Genintern.register_intern0 wit intern_fun in
+ let () = Genintern.register_subst0 wit subst_fun in
+ (* No need to register a value tag for it via register_val0 since we will
+ never access this genarg directly. *)
+ let interp_fun ist tac =
+ let args = List.map (fun id -> Id.Map.get id ist.Geninterp.lfun) tac.tacval_var in
+ let tac = MLTacMap.get tac.tacval_tac !ml_table in
+ tac args
+ in
+ let () = Geninterp.register_interp0 wit interp_fun in
+ (fun v -> Genarg.in_gen (Genarg.Glbwit wit) v)
+
+
+let ml_val_tactic_extend ~plugin ~name ~local ?deprecation sign tac =
+ let open Tacexpr in
+ let tac args = cast_ml sign tac args in
+ let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in
+ let len = ml_sig_len sign in
+ let vars = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in
+ let body = TacGeneric (in_tacval { tacval_tac = ml_tactic_name; tacval_var = vars }) in
+ let vars = List.map (fun id -> Name id) vars in
+ let body = Tacexpr.TacFun (vars, Tacexpr.TacArg (CAst.make body)) in
+ let id = Names.Id.of_string name in
+ let obj () = Tacenv.register_ltac true local id body ?deprecation in
+ let () = assert (not @@ MLTacMap.mem ml_tactic_name !ml_table) in
+ let () = ml_table := MLTacMap.add ml_tactic_name tac !ml_table in
+ Mltop.declare_cache_obj obj plugin
(** ARGUMENT EXTEND *)
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index ce38431a18..6ee3ce091b 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -69,6 +69,25 @@ val print_ltacs : unit -> unit
val print_located_tactic : Libnames.qualid -> unit
(** Display the absolute name of a tactic. *)
+(** {5 Low-level registering of tactics} *)
+
+type (_, 'a) ml_ty_sig =
+| MLTyNil : ('a, 'a) ml_ty_sig
+| MLTyArg : ('r, 'a) ml_ty_sig -> (Geninterp.Val.t -> 'r, 'a) ml_ty_sig
+
+val ml_tactic_extend : plugin:string -> name:string -> local:locality_flag ->
+ ?deprecation:Deprecation.t -> ('r, unit Proofview.tactic) ml_ty_sig -> 'r -> unit
+(** Helper function to define directly an Ltac function in OCaml without any
+ associated parsing rule nor further shenanigans. The Ltac function will be
+ defined as [name] in the Coq file that loads the ML plugin where this
+ function is called. It will have the arity given by the [ml_ty_sig]
+ argument. *)
+
+val ml_val_tactic_extend : plugin:string -> name:string -> local:locality_flag ->
+ ?deprecation:Deprecation.t -> ('r, Geninterp.Val.t Ftactic.t) ml_ty_sig -> 'r -> unit
+(** Same as {!ml_tactic_extend} but the function can return an argument
+ instead. *)
+
(** {5 TACTIC EXTEND} *)
type _ ty_sig =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index dda7f0742c..6debc7d9b9 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1895,8 +1895,7 @@ module Value = struct
let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
of_tacvalue closure
- (** Apply toplevel tactic values *)
- let apply (f : value) (args: value list) =
+ let apply_expr f args =
let fold arg (i, vars, lfun) =
let id = Id.of_string ("x" ^ string_of_int i) in
let x = Reference (ArgVar CAst.(make id)) in
@@ -1905,9 +1904,18 @@ module Value = struct
let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
let lfun = Id.Map.add (Id.of_string "F") f lfun in
let ist = { (default_ist ()) with lfun = lfun; } in
- let tac = TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) in
+ ist, TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args)))
+
+
+ (** Apply toplevel tactic values *)
+ let apply (f : value) (args: value list) =
+ let ist, tac = apply_expr f args in
eval_tactic_ist ist tac
+ let apply_val (f : value) (args: value list) =
+ let ist, tac = apply_expr f args in
+ val_interp ist tac
+
end
(* globalization + interpretation *)
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index ce34356a37..cbb17bf0fa 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -29,6 +29,7 @@ sig
val of_closure : Geninterp.interp_sign -> glob_tactic_expr -> t
val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a
val apply : t -> t list -> unit Proofview.tactic
+ val apply_val : t -> t list -> t Ftactic.t
end
(** Values for interpretation *)
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 7e4c4ce5c6..ee2c87d19a 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -128,249 +128,142 @@ let selecti s m =
*)
module M = struct
(**
- * Location of the Coq libraries.
- *)
-
- let logic_dir = ["Coq"; "Logic"; "Decidable"]
-
- let mic_modules =
- [ ["Coq"; "Lists"; "List"]
- ; ["Coq"; "micromega"; "ZMicromega"]
- ; ["Coq"; "micromega"; "Tauto"]
- ; ["Coq"; "micromega"; "DeclConstant"]
- ; ["Coq"; "micromega"; "RingMicromega"]
- ; ["Coq"; "micromega"; "EnvRing"]
- ; ["Coq"; "micromega"; "ZMicromega"]
- ; ["Coq"; "micromega"; "RMicromega"]
- ; ["Coq"; "micromega"; "Tauto"]
- ; ["Coq"; "micromega"; "RingMicromega"]
- ; ["Coq"; "micromega"; "EnvRing"]
- ; ["Coq"; "QArith"; "QArith_base"]
- ; ["Coq"; "Reals"; "Rdefinitions"]
- ; ["Coq"; "Reals"; "Rpow_def"]
- ; ["LRing_normalise"] ]
-
- [@@@ocaml.warning "-3"]
-
- let coq_modules =
- Coqlib.(
- init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
- @ mic_modules)
-
- let bin_module = [["Coq"; "Numbers"; "BinNums"]]
-
- let r_modules =
- [ ["Coq"; "Reals"; "Rdefinitions"]
- ; ["Coq"; "Reals"; "Rpow_def"]
- ; ["Coq"; "Reals"; "Raxioms"]
- ; ["Coq"; "QArith"; "Qreals"] ]
-
- let z_modules = [["Coq"; "ZArith"; "BinInt"]]
-
- (**
* Initialization : a large amount of Caml symbols are derived from
* ZMicromega.v
*)
- let gen_constant_in_modules s m n =
+ let constr_of_ref str =
EConstr.of_constr
- ( UnivGen.constr_of_monomorphic_global
- @@ Coqlib.gen_reference_in_modules s m n )
-
- let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules
-
- [@@@ocaml.warning "+3"]
-
- let constant = gen_constant_in_modules "ZMicromega" coq_modules
- let bin_constant = gen_constant_in_modules "ZMicromega" bin_module
- let r_constant = gen_constant_in_modules "ZMicromega" r_modules
- let z_constant = gen_constant_in_modules "ZMicromega" z_modules
- let m_constant = gen_constant_in_modules "ZMicromega" mic_modules
- let coq_and = lazy (init_constant "and")
- let coq_or = lazy (init_constant "or")
- let coq_not = lazy (init_constant "not")
- let coq_iff = lazy (init_constant "iff")
- let coq_True = lazy (init_constant "True")
- let coq_False = lazy (init_constant "False")
- let coq_cons = lazy (constant "cons")
- let coq_nil = lazy (constant "nil")
- let coq_list = lazy (constant "list")
- let coq_O = lazy (init_constant "O")
- let coq_S = lazy (init_constant "S")
- let coq_nat = lazy (init_constant "nat")
- let coq_unit = lazy (init_constant "unit")
+ (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref str))
+
+ let coq_and = lazy (constr_of_ref "core.and.type")
+ let coq_or = lazy (constr_of_ref "core.or.type")
+ let coq_not = lazy (constr_of_ref "core.not.type")
+ let coq_iff = lazy (constr_of_ref "core.iff.type")
+ let coq_True = lazy (constr_of_ref "core.True.type")
+ let coq_False = lazy (constr_of_ref "core.False.type")
+ let coq_cons = lazy (constr_of_ref "core.list.cons")
+ let coq_nil = lazy (constr_of_ref "core.list.nil")
+ let coq_list = lazy (constr_of_ref "core.list.type")
+ let coq_O = lazy (constr_of_ref "num.nat.O")
+ let coq_S = lazy (constr_of_ref "num.nat.S")
+ let coq_nat = lazy (constr_of_ref "num.nat.type")
+ let coq_unit = lazy (constr_of_ref "core.unit.type")
(* let coq_option = lazy (init_constant "option")*)
- let coq_None = lazy (init_constant "None")
- let coq_tt = lazy (init_constant "tt")
- let coq_Inl = lazy (init_constant "inl")
- let coq_Inr = lazy (init_constant "inr")
- let coq_N0 = lazy (bin_constant "N0")
- let coq_Npos = lazy (bin_constant "Npos")
- let coq_xH = lazy (bin_constant "xH")
- let coq_xO = lazy (bin_constant "xO")
- let coq_xI = lazy (bin_constant "xI")
- let coq_Z = lazy (bin_constant "Z")
- let coq_ZERO = lazy (bin_constant "Z0")
- let coq_POS = lazy (bin_constant "Zpos")
- let coq_NEG = lazy (bin_constant "Zneg")
- let coq_Q = lazy (constant "Q")
- let coq_R = lazy (constant "R")
- let coq_Qmake = lazy (constant "Qmake")
- let coq_Rcst = lazy (constant "Rcst")
- let coq_C0 = lazy (m_constant "C0")
- let coq_C1 = lazy (m_constant "C1")
- let coq_CQ = lazy (m_constant "CQ")
- let coq_CZ = lazy (m_constant "CZ")
- let coq_CPlus = lazy (m_constant "CPlus")
- let coq_CMinus = lazy (m_constant "CMinus")
- let coq_CMult = lazy (m_constant "CMult")
- let coq_CPow = lazy (m_constant "CPow")
- let coq_CInv = lazy (m_constant "CInv")
- let coq_COpp = lazy (m_constant "COpp")
- let coq_R0 = lazy (constant "R0")
- let coq_R1 = lazy (constant "R1")
- let coq_proofTerm = lazy (constant "ZArithProof")
- let coq_doneProof = lazy (constant "DoneProof")
- let coq_ratProof = lazy (constant "RatProof")
- let coq_cutProof = lazy (constant "CutProof")
- let coq_enumProof = lazy (constant "EnumProof")
- let coq_ExProof = lazy (constant "ExProof")
- let coq_Zgt = lazy (z_constant "Z.gt")
- let coq_Zge = lazy (z_constant "Z.ge")
- let coq_Zle = lazy (z_constant "Z.le")
- let coq_Zlt = lazy (z_constant "Z.lt")
- let coq_Eq = lazy (init_constant "eq")
- let coq_Zplus = lazy (z_constant "Z.add")
- let coq_Zminus = lazy (z_constant "Z.sub")
- let coq_Zopp = lazy (z_constant "Z.opp")
- let coq_Zmult = lazy (z_constant "Z.mul")
- let coq_Zpower = lazy (z_constant "Z.pow")
- let coq_Qle = lazy (constant "Qle")
- let coq_Qlt = lazy (constant "Qlt")
- let coq_Qeq = lazy (constant "Qeq")
- let coq_Qplus = lazy (constant "Qplus")
- let coq_Qminus = lazy (constant "Qminus")
- let coq_Qopp = lazy (constant "Qopp")
- let coq_Qmult = lazy (constant "Qmult")
- let coq_Qpower = lazy (constant "Qpower")
- let coq_Rgt = lazy (r_constant "Rgt")
- let coq_Rge = lazy (r_constant "Rge")
- let coq_Rle = lazy (r_constant "Rle")
- let coq_Rlt = lazy (r_constant "Rlt")
- let coq_Rplus = lazy (r_constant "Rplus")
- let coq_Rminus = lazy (r_constant "Rminus")
- let coq_Ropp = lazy (r_constant "Ropp")
- let coq_Rmult = lazy (r_constant "Rmult")
- let coq_Rinv = lazy (r_constant "Rinv")
- let coq_Rpower = lazy (r_constant "pow")
- let coq_powerZR = lazy (r_constant "powerRZ")
- let coq_IZR = lazy (r_constant "IZR")
- let coq_IQR = lazy (r_constant "Q2R")
- let coq_PEX = lazy (constant "PEX")
- let coq_PEc = lazy (constant "PEc")
- let coq_PEadd = lazy (constant "PEadd")
- let coq_PEopp = lazy (constant "PEopp")
- let coq_PEmul = lazy (constant "PEmul")
- let coq_PEsub = lazy (constant "PEsub")
- let coq_PEpow = lazy (constant "PEpow")
- let coq_PX = lazy (constant "PX")
- let coq_Pc = lazy (constant "Pc")
- let coq_Pinj = lazy (constant "Pinj")
- let coq_OpEq = lazy (constant "OpEq")
- let coq_OpNEq = lazy (constant "OpNEq")
- let coq_OpLe = lazy (constant "OpLe")
- let coq_OpLt = lazy (constant "OpLt")
- let coq_OpGe = lazy (constant "OpGe")
- let coq_OpGt = lazy (constant "OpGt")
- let coq_PsatzIn = lazy (constant "PsatzIn")
- let coq_PsatzSquare = lazy (constant "PsatzSquare")
- let coq_PsatzMulE = lazy (constant "PsatzMulE")
- let coq_PsatzMultC = lazy (constant "PsatzMulC")
- let coq_PsatzAdd = lazy (constant "PsatzAdd")
- let coq_PsatzC = lazy (constant "PsatzC")
- let coq_PsatzZ = lazy (constant "PsatzZ")
+ let coq_None = lazy (constr_of_ref "core.option.None")
+ let coq_tt = lazy (constr_of_ref "core.unit.tt")
+ let coq_Inl = lazy (constr_of_ref "core.sum.inl")
+ let coq_Inr = lazy (constr_of_ref "core.sum.inr")
+ let coq_N0 = lazy (constr_of_ref "num.N.N0")
+ let coq_Npos = lazy (constr_of_ref "num.N.Npos")
+ let coq_xH = lazy (constr_of_ref "num.pos.xH")
+ let coq_xO = lazy (constr_of_ref "num.pos.xO")
+ let coq_xI = lazy (constr_of_ref "num.pos.xI")
+ let coq_Z = lazy (constr_of_ref "num.Z.type")
+ let coq_ZERO = lazy (constr_of_ref "num.Z.Z0")
+ let coq_POS = lazy (constr_of_ref "num.Z.Zpos")
+ let coq_NEG = lazy (constr_of_ref "num.Z.Zneg")
+ let coq_Q = lazy (constr_of_ref "rat.Q.type")
+ let coq_Qmake = lazy (constr_of_ref "rat.Q.Qmake")
+ let coq_R = lazy (constr_of_ref "reals.R.type")
+ let coq_Rcst = lazy (constr_of_ref "micromega.Rcst.type")
+ let coq_C0 = lazy (constr_of_ref "micromega.Rcst.C0")
+ let coq_C1 = lazy (constr_of_ref "micromega.Rcst.C1")
+ let coq_CQ = lazy (constr_of_ref "micromega.Rcst.CQ")
+ let coq_CZ = lazy (constr_of_ref "micromega.Rcst.CZ")
+ let coq_CPlus = lazy (constr_of_ref "micromega.Rcst.CPlus")
+ let coq_CMinus = lazy (constr_of_ref "micromega.Rcst.CMinus")
+ let coq_CMult = lazy (constr_of_ref "micromega.Rcst.CMult")
+ let coq_CPow = lazy (constr_of_ref "micromega.Rcst.CPow")
+ let coq_CInv = lazy (constr_of_ref "micromega.Rcst.CInv")
+ let coq_COpp = lazy (constr_of_ref "micromega.Rcst.COpp")
+ let coq_R0 = lazy (constr_of_ref "reals.R.R0")
+ let coq_R1 = lazy (constr_of_ref "reals.R.R1")
+ let coq_proofTerm = lazy (constr_of_ref "micromega.ZArithProof.type")
+ let coq_doneProof = lazy (constr_of_ref "micromega.ZArithProof.DoneProof")
+ let coq_ratProof = lazy (constr_of_ref "micromega.ZArithProof.RatProof")
+ let coq_cutProof = lazy (constr_of_ref "micromega.ZArithProof.CutProof")
+ let coq_enumProof = lazy (constr_of_ref "micromega.ZArithProof.EnumProof")
+ let coq_ExProof = lazy (constr_of_ref "micromega.ZArithProof.ExProof")
+ let coq_Zgt = lazy (constr_of_ref "num.Z.gt")
+ let coq_Zge = lazy (constr_of_ref "num.Z.ge")
+ let coq_Zle = lazy (constr_of_ref "num.Z.le")
+ let coq_Zlt = lazy (constr_of_ref "num.Z.lt")
+ let coq_Eq = lazy (constr_of_ref "core.eq.type")
+ let coq_Zplus = lazy (constr_of_ref "num.Z.add")
+ let coq_Zminus = lazy (constr_of_ref "num.Z.sub")
+ let coq_Zopp = lazy (constr_of_ref "num.Z.opp")
+ let coq_Zmult = lazy (constr_of_ref "num.Z.mul")
+ let coq_Zpower = lazy (constr_of_ref "num.Z.pow")
+ let coq_Qle = lazy (constr_of_ref "rat.Q.Qle")
+ let coq_Qlt = lazy (constr_of_ref "rat.Q.Qlt")
+ let coq_Qeq = lazy (constr_of_ref "rat.Q.Qeq")
+ let coq_Qplus = lazy (constr_of_ref "rat.Q.Qplus")
+ let coq_Qminus = lazy (constr_of_ref "rat.Q.Qminus")
+ let coq_Qopp = lazy (constr_of_ref "rat.Q.Qopp")
+ let coq_Qmult = lazy (constr_of_ref "rat.Q.Qmult")
+ let coq_Qpower = lazy (constr_of_ref "rat.Q.Qpower")
+ let coq_Rgt = lazy (constr_of_ref "reals.R.Rgt")
+ let coq_Rge = lazy (constr_of_ref "reals.R.Rge")
+ let coq_Rle = lazy (constr_of_ref "reals.R.Rle")
+ let coq_Rlt = lazy (constr_of_ref "reals.R.Rlt")
+ let coq_Rplus = lazy (constr_of_ref "reals.R.Rplus")
+ let coq_Rminus = lazy (constr_of_ref "reals.R.Rminus")
+ let coq_Ropp = lazy (constr_of_ref "reals.R.Ropp")
+ let coq_Rmult = lazy (constr_of_ref "reals.R.Rmult")
+ let coq_Rinv = lazy (constr_of_ref "reals.R.Rinv")
+ let coq_Rpower = lazy (constr_of_ref "reals.R.pow")
+ let coq_powerZR = lazy (constr_of_ref "reals.R.powerRZ")
+ let coq_IZR = lazy (constr_of_ref "reals.R.IZR")
+ let coq_IQR = lazy (constr_of_ref "reals.R.Q2R")
+ let coq_PEX = lazy (constr_of_ref "micromega.PExpr.PEX")
+ let coq_PEc = lazy (constr_of_ref "micromega.PExpr.PEc")
+ let coq_PEadd = lazy (constr_of_ref "micromega.PExpr.PEadd")
+ let coq_PEopp = lazy (constr_of_ref "micromega.PExpr.PEopp")
+ let coq_PEmul = lazy (constr_of_ref "micromega.PExpr.PEmul")
+ let coq_PEsub = lazy (constr_of_ref "micromega.PExpr.PEsub")
+ let coq_PEpow = lazy (constr_of_ref "micromega.PExpr.PEpow")
+ let coq_PX = lazy (constr_of_ref "micromega.Pol.PX")
+ let coq_Pc = lazy (constr_of_ref "micromega.Pol.Pc")
+ let coq_Pinj = lazy (constr_of_ref "micromega.Pol.Pinj")
+ let coq_OpEq = lazy (constr_of_ref "micromega.Op2.OpEq")
+ let coq_OpNEq = lazy (constr_of_ref "micromega.Op2.OpNEq")
+ let coq_OpLe = lazy (constr_of_ref "micromega.Op2.OpLe")
+ let coq_OpLt = lazy (constr_of_ref "micromega.Op2.OpLt")
+ let coq_OpGe = lazy (constr_of_ref "micromega.Op2.OpGe")
+ let coq_OpGt = lazy (constr_of_ref "micromega.Op2.OpGt")
+ let coq_PsatzIn = lazy (constr_of_ref "micromega.Psatz.PsatzIn")
+ let coq_PsatzSquare = lazy (constr_of_ref "micromega.Psatz.PsatzSquare")
+ let coq_PsatzMulE = lazy (constr_of_ref "micromega.Psatz.PsatzMulE")
+ let coq_PsatzMultC = lazy (constr_of_ref "micromega.Psatz.PsatzMulC")
+ let coq_PsatzAdd = lazy (constr_of_ref "micromega.Psatz.PsatzAdd")
+ let coq_PsatzC = lazy (constr_of_ref "micromega.Psatz.PsatzC")
+ let coq_PsatzZ = lazy (constr_of_ref "micromega.Psatz.PsatzZ")
(* let coq_GT = lazy (m_constant "GT")*)
- let coq_DeclaredConstant = lazy (m_constant "DeclaredConstant")
-
- let coq_TT =
- lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
- "TT")
-
- let coq_FF =
- lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
- "FF")
-
- let coq_And =
- lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
- "Cj")
+ let coq_DeclaredConstant =
+ lazy (constr_of_ref "micromega.DeclaredConstant.type")
- let coq_Or =
- lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
- "D")
-
- let coq_Neg =
- lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
- "N")
-
- let coq_Atom =
- lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
- "A")
-
- let coq_X =
- lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
- "X")
-
- let coq_Impl =
- lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
- "I")
-
- let coq_Formula =
- lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
- "BFormula")
+ let coq_TT = lazy (constr_of_ref "micromega.GFormula.TT")
+ let coq_FF = lazy (constr_of_ref "micromega.GFormula.FF")
+ let coq_And = lazy (constr_of_ref "micromega.GFormula.Cj")
+ let coq_Or = lazy (constr_of_ref "micromega.GFormula.D")
+ let coq_Neg = lazy (constr_of_ref "micromega.GFormula.N")
+ let coq_Atom = lazy (constr_of_ref "micromega.GFormula.A")
+ let coq_X = lazy (constr_of_ref "micromega.GFormula.X")
+ let coq_Impl = lazy (constr_of_ref "micromega.GFormula.I")
+ let coq_Formula = lazy (constr_of_ref "micromega.BFormula.type")
(**
* Initialization : a few Caml symbols are derived from other libraries;
* QMicromega, ZArithRing, RingMicromega.
*)
- let coq_QWitness =
- lazy
- (gen_constant_in_modules "QMicromega"
- [["Coq"; "micromega"; "QMicromega"]]
- "QWitness")
-
- let coq_Build =
- lazy
- (gen_constant_in_modules "RingMicromega"
- [["Coq"; "micromega"; "RingMicromega"]; ["RingMicromega"]]
- "Build_Formula")
-
- let coq_Cstr =
- lazy
- (gen_constant_in_modules "RingMicromega"
- [["Coq"; "micromega"; "RingMicromega"]; ["RingMicromega"]]
- "Formula")
+ let coq_QWitness = lazy (constr_of_ref "micromega.QWitness.type")
+ let coq_Build = lazy (constr_of_ref "micromega.Formula.Build_Formula")
+ let coq_Cstr = lazy (constr_of_ref "micromega.Formula.type")
(**
* Parsing and dumping : transformation functions between Caml and Coq
@@ -1318,29 +1211,10 @@ end
open M
-let coq_Branch =
- lazy
- (gen_constant_in_modules "VarMap"
- [["Coq"; "micromega"; "VarMap"]; ["VarMap"]]
- "Branch")
-
-let coq_Elt =
- lazy
- (gen_constant_in_modules "VarMap"
- [["Coq"; "micromega"; "VarMap"]; ["VarMap"]]
- "Elt")
-
-let coq_Empty =
- lazy
- (gen_constant_in_modules "VarMap"
- [["Coq"; "micromega"; "VarMap"]; ["VarMap"]]
- "Empty")
-
-let coq_VarMap =
- lazy
- (gen_constant_in_modules "VarMap"
- [["Coq"; "micromega"; "VarMap"]; ["VarMap"]]
- "t")
+let coq_Branch = lazy (constr_of_ref "micromega.VarMap.Branch")
+let coq_Elt = lazy (constr_of_ref "micromega.VarMap.Elt")
+let coq_Empty = lazy (constr_of_ref "micromega.VarMap.Empty")
+let coq_VarMap = lazy (constr_of_ref "micromega.VarMap.type")
let rec dump_varmap typ m =
match m with
@@ -1900,13 +1774,7 @@ let micromega_order_changer cert env ff =
[ ( "__ff"
, ff
, EConstr.mkApp (Lazy.force coq_Formula, [|formula_typ|]) )
- ; ( "__varmap"
- , vm
- , EConstr.mkApp
- ( gen_constant_in_modules "VarMap"
- [["Coq"; "micromega"; "VarMap"]; ["VarMap"]]
- "t"
- , [|typ|] ) )
+ ; ("__varmap", vm, EConstr.mkApp (Lazy.force coq_VarMap, [|typ|]))
; ("__wit", cert, cert_typ) ]
(Tacmach.New.pf_concl gl))
(* Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)*)
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 0307728819..60af804c1b 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -349,8 +349,8 @@ let interp_index ist gl idx =
begin match Tacinterp.Value.to_constr v with
| Some c ->
let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in
- begin match Notation.uninterp_prim_token rc with
- | _, Constrexpr.Numeral n when NumTok.Signed.is_int n ->
+ begin match Notation.uninterp_prim_token rc (None, []) with
+ | Constrexpr.Numeral n, _ when NumTok.Signed.is_int n ->
int_of_string (NumTok.Signed.to_string n)
| _ -> raise Not_found
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 21:47:33 +0000