aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/json.ml3
-rw-r--r--plugins/extraction/ocaml.ml5
-rw-r--r--plugins/firstorder/g_ground.ml46
-rw-r--r--plugins/funind/recdef.ml4
-rw-r--r--plugins/ltac/LtacDummy.v2
-rw-r--r--plugins/ltac/ltac_dummy.ml0
-rw-r--r--plugins/ltac/ltac_dummy.mli0
-rw-r--r--plugins/ltac/ltac_plugin.mlpack1
-rw-r--r--plugins/ltac/vo.itarget1
-rw-r--r--plugins/micromega/coq_micromega.ml18
-rw-r--r--plugins/ssrmatching/ssrmatching.ml4103
-rw-r--r--plugins/ssrmatching/ssrmatching.mli2
12 files changed, 82 insertions, 63 deletions
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index 8874afef33..e43c47d050 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -142,7 +142,8 @@ let rec json_expr env = function
("what", json_str "fix:item");
("name", json_id fi);
("body", json_function env' ti)
- ]) (Array.map2 (fun a b -> a,b) ids' defs)))
+ ]) (Array.map2 (fun a b -> a,b) ids' defs)));
+ ("for", json_int i);
]
| MLexn s -> json_dict [
("what", json_str "expr:exception");
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 1c29a9bc24..5d10cb939d 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -618,12 +618,13 @@ let rec pp_specif = function
with Not_found -> pp_spec s)
| (l,Smodule mt) ->
let def = pp_module_type [] mt in
- let def' = pp_module_type [] mt in
let name = pp_modname (MPdot (top_visible_mp (), l)) in
hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++
(try
let ren = Common.check_duplicate (top_visible_mp ()) l in
- fnl () ++ hov 1 (str ("module "^ren^" :") ++ fnl () ++ def')
+ fnl () ++
+ hov 1 (str ("module "^ren^" :") ++ spc () ++
+ str "module type of struct include " ++ name ++ str " end")
with Not_found -> Pp.mt ())
| (l,Smodtype mt) ->
let def = pp_module_type [] mt in
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 95095b09cb..43fac8ad83 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -116,9 +116,9 @@ open Pp
open Genarg
open Ppconstr
open Printer
-let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_reference l
-let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l
-let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
+let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_reference
+let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x)))
+let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global
let warn_deprecated_syntax =
CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated"
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 62f3071151..fa84e4ddf3 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1538,7 +1538,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
begin
if do_observe ()
then Feedback.msg_debug (str "Cannot create equation Lemma " ++ CErrors.print e)
- else anomaly (Pp.str "Cannot create equation Lemma")
+ else CErrors.errorlabstrm "Cannot create equation Lemma"
+ (str "Cannot create equation lemma." ++ spc () ++
+ str "This may be because the function is nested-recursive.")
;
true
end
diff --git a/plugins/ltac/LtacDummy.v b/plugins/ltac/LtacDummy.v
new file mode 100644
index 0000000000..4f96bbaeb9
--- /dev/null
+++ b/plugins/ltac/LtacDummy.v
@@ -0,0 +1,2 @@
+(* The sole reason of this file is to trick coq's build system to build the dummy ltac plugin *)
+Declare ML Module "ltac_plugin".
diff --git a/plugins/ltac/ltac_dummy.ml b/plugins/ltac/ltac_dummy.ml
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/plugins/ltac/ltac_dummy.ml
diff --git a/plugins/ltac/ltac_dummy.mli b/plugins/ltac/ltac_dummy.mli
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/plugins/ltac/ltac_dummy.mli
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
new file mode 100644
index 0000000000..6efb477cce
--- /dev/null
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -0,0 +1 @@
+Ltac_dummy
diff --git a/plugins/ltac/vo.itarget b/plugins/ltac/vo.itarget
new file mode 100644
index 0000000000..4eff76566a
--- /dev/null
+++ b/plugins/ltac/vo.itarget
@@ -0,0 +1 @@
+LtacDummy.vo
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index a063cbbfe3..e4b58a56f9 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1517,27 +1517,27 @@ let rec apply_ids t ids =
| [] -> t
| i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids
-let coq_Node =
+let coq_Node = lazy
(Coqlib.gen_constant_in_modules "VarMap"
[["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node")
-let coq_Leaf =
+let coq_Leaf = lazy
(Coqlib.gen_constant_in_modules "VarMap"
[["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf")
-let coq_Empty =
+let coq_Empty = lazy
(Coqlib.gen_constant_in_modules "VarMap"
[["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty")
-let coq_VarMap =
+let coq_VarMap = lazy
(Coqlib.gen_constant_in_modules "VarMap"
[["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t")
let rec dump_varmap typ m =
match m with
- | Mc.Empty -> Term.mkApp(coq_Empty,[| typ |])
- | Mc.Leaf v -> Term.mkApp(coq_Leaf,[| typ; v|])
- | Mc.Node(l,o,r) ->
- Term.mkApp (coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |])
+ | Mc.Empty -> Term.mkApp(Lazy.force coq_Empty,[| typ |])
+ | Mc.Leaf v -> Term.mkApp(Lazy.force coq_Leaf,[| typ; v|])
+ | Mc.Node(l,o,r) ->
+ Term.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |])
let vm_of_list env =
@@ -1709,7 +1709,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*
(set
[
("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
- ("__varmap", vm, Term.mkApp( coq_VarMap, [|spec.typ|]));
+ ("__varmap", vm, Term.mkApp(Lazy.force coq_VarMap, [|spec.typ|]));
("__wit", cert, cert_typ)
]
(Tacmach.pf_concl gl))
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index a34fa4cae7..d21223d43d 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -112,8 +112,7 @@ let guard_term ch1 s i = match s.[i] with
(* The call 'guard s i' should return true if the contents of s *)
(* starting at i need bracketing to avoid ambiguities. *)
let pr_guarded guard prc c =
- msg_with Format.str_formatter (prc c);
- let s = Format.flush_str_formatter () ^ "$" in
+ let s = Pp.string_of_ppcmds (prc c) ^ "$" in
if guard s (skip_wschars s 0) then pr_paren prc c else prc c
(* More sensible names for constr printers *)
let pr_constr = pr_constr
@@ -355,7 +354,7 @@ let nf_open_term sigma0 ise c =
!s', Evd.evar_universe_context s, c'
let unif_end env sigma0 ise0 pt ok =
- let ise = Evarconv.consider_remaining_unif_problems env ise0 in
+ let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in
let s, uc, t = nf_open_term sigma0 ise pt in
let ise1 = create_evar_defs s in
let ise1 = Evd.set_universe_context ise1 uc in
@@ -391,7 +390,8 @@ let iter_constr_LR f c = match kind_of_term c with
| Case (_, p, v, b) -> f v; f p; Array.iter f b
| Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) ->
for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done
- | _ -> ()
+ | Proj(_,a) -> f a
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> ()
(* The comparison used to determine which subterms matches is KEYED *)
(* CONVERSION. This looks for convertible terms that either have the same *)
@@ -435,7 +435,7 @@ let proj_nparams c =
try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0
let isFixed c = match kind_of_term c with
- | Var _ | Ind _ | Construct _ | Const _ -> true
+ | Var _ | Ind _ | Construct _ | Const _ | Proj _ -> true
| _ -> false
let isRigid c = match kind_of_term c with
@@ -487,6 +487,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p =
let np = proj_nparams p in
if np = 0 || np > List.length a then KpatConst, f, a else
let a1, a2 = List.chop np a in KpatProj p, applist(f, a1), a2
+ | Proj (p,arg) -> KpatProj (Projection.constant p), f, a
| Var _ | Ind _ | Construct _ -> KpatFixed, f, a
| Evar (k, _) ->
if Evd.mem sigma0 k then KpatEvar k, f, a else
@@ -524,7 +525,13 @@ let nb_cs_proj_args pc f u =
try match kind_of_term f with
| Prod _ -> na Prod_cs
| Sort s -> na (Sort_cs (family_of_sort s))
- | Const (c',_) when Constant.equal c' pc -> Array.length (snd (destApp u.up_f))
+ | Const (c',_) when Constant.equal c' pc ->
+ begin match kind_of_term u.up_f with
+ | App(_,args) -> Array.length args
+ | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be
+ the number of arguments including the projected *)
+ | _ -> assert false
+ end
| Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (global_of_constr f))
| _ -> -1
with Not_found -> -1
@@ -567,6 +574,10 @@ let filter_upat i0 f n u fpats =
if np < na then fpats else
let () = if !i0 < np then i0 := n in (u, np) :: fpats
+let eq_prim_proj c t = match kind_of_term t with
+ | Proj(p,_) -> Constant.equal (Projection.constant p) c
+ | _ -> false
+
let filter_upat_FO i0 f n u fpats =
let np = nb_args u.up_FO in
if n < np then fpats else
@@ -577,7 +588,7 @@ let filter_upat_FO i0 f n u fpats =
| KpatLet -> isLetIn f
| KpatLam -> isLambda f
| KpatRigid -> isRigid f
- | KpatProj pc -> Term.eq_constr f (mkConst pc)
+ | KpatProj pc -> Term.eq_constr f (mkConst pc) || eq_prim_proj pc f
| KpatFlex -> i0 := n; true in
if ok then begin if !i0 < np then i0 := np; (u, np) :: fpats end else fpats
@@ -908,9 +919,47 @@ let glob_ssrterm gs = function
fst x, Some c
| ct -> ct
+(* This piece of code asserts the following notations are reserved *)
+(* Reserved Notation "( a 'in' b )" (at level 0). *)
+(* Reserved Notation "( a 'as' b )" (at level 0). *)
+(* Reserved Notation "( a 'in' b 'in' c )" (at level 0). *)
+(* Reserved Notation "( a 'as' b 'in' c )" (at level 0). *)
+let glob_cpattern gs p =
+ pp(lazy(str"globbing pattern: " ++ pr_term p));
+ let glob x = snd (glob_ssrterm gs (mk_lterm x)) in
+ let encode k s l =
+ let name = Name (id_of_string ("_ssrpat_" ^ s)) in
+ k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None) in
+ let bind_in t1 t2 =
+ let d = dummy_loc in let n = Name (destCVar t1) in
+ fst (glob (mkCCast d (mkCHole d) (mkCLambda d n (mkCHole d) t2))) in
+ let check_var t2 = if not (isCVar t2) then
+ loc_error (constr_loc t2) "Only identifiers are allowed here" in
+ match p with
+ | _, (_, None) as x -> x
+ | k, (v, Some t) as orig ->
+ if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else
+ match t with
+ | CNotation(_, "( _ in _ )", ([t1; t2], [], [])) ->
+ (try match glob t1, glob t2 with
+ | (r1, None), (r2, None) -> encode k "In" [r1;r2]
+ | (r1, Some _), (r2, Some _) when isCVar t1 ->
+ encode k "In" [r1; r2; bind_in t1 t2]
+ | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2]
+ | _ -> CErrors.anomaly (str"where are we?")
+ with _ when isCVar t1 -> encode k "In" [bind_in t1 t2])
+ | CNotation(_, "( _ in _ in _ )", ([t1; t2; t3], [], [])) ->
+ check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3]
+ | CNotation(_, "( _ as _ )", ([t1; t2], [], [])) ->
+ encode k "As" [fst (glob t1); fst (glob t2)]
+ | CNotation(_, "( _ as _ in _ )", ([t1; t2; t3], [], [])) ->
+ check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3]
+ | _ -> glob_ssrterm gs orig
+;;
+
let glob_rpattern s p =
match p with
- | T t -> T (glob_ssrterm s t)
+ | T t -> T (glob_cpattern s t)
| In_T t -> In_T (glob_ssrterm s t)
| X_In_T(x,t) -> X_In_T (x,glob_ssrterm s t)
| In_X_In_T(x,t) -> In_X_In_T (x,glob_ssrterm s t)
@@ -995,44 +1044,6 @@ let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with
| _ -> ' '
let ssrtermkind = Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
-(* This piece of code asserts the following notations are reserved *)
-(* Reserved Notation "( a 'in' b )" (at level 0). *)
-(* Reserved Notation "( a 'as' b )" (at level 0). *)
-(* Reserved Notation "( a 'in' b 'in' c )" (at level 0). *)
-(* Reserved Notation "( a 'as' b 'in' c )" (at level 0). *)
-let glob_cpattern gs p =
- pp(lazy(str"globbing pattern: " ++ pr_term p));
- let glob x = snd (glob_ssrterm gs (mk_lterm x)) in
- let encode k s l =
- let name = Name (id_of_string ("_ssrpat_" ^ s)) in
- k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None) in
- let bind_in t1 t2 =
- let d = dummy_loc in let n = Name (destCVar t1) in
- fst (glob (mkCCast d (mkCHole d) (mkCLambda d n (mkCHole d) t2))) in
- let check_var t2 = if not (isCVar t2) then
- loc_error (constr_loc t2) "Only identifiers are allowed here" in
- match p with
- | _, (_, None) as x -> x
- | k, (v, Some t) as orig ->
- if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else
- match t with
- | CNotation(_, "( _ in _ )", ([t1; t2], [], [])) ->
- (try match glob t1, glob t2 with
- | (r1, None), (r2, None) -> encode k "In" [r1;r2]
- | (r1, Some _), (r2, Some _) when isCVar t1 ->
- encode k "In" [r1; r2; bind_in t1 t2]
- | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2]
- | _ -> CErrors.anomaly (str"where are we?")
- with _ when isCVar t1 -> encode k "In" [bind_in t1 t2])
- | CNotation(_, "( _ in _ in _ )", ([t1; t2; t3], [], [])) ->
- check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3]
- | CNotation(_, "( _ as _ )", ([t1; t2], [], [])) ->
- encode k "As" [fst (glob t1); fst (glob t2)]
- | CNotation(_, "( _ as _ in _ )", ([t1; t2; t3], [], [])) ->
- check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3]
- | _ -> glob_ssrterm gs orig
-;;
-
let interp_ssrterm _ gl t = Tacmach.project gl, t
ARGUMENT EXTEND cpattern
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 74a603e51c..288a04e60a 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -213,7 +213,7 @@ val assert_done : 'a option ref -> 'a
(** Very low level APIs.
these are calls to evarconv's [the_conv_x] followed by
- [consider_remaining_unif_problems] and [resolve_typeclasses].
+ [solve_unif_constraints_with_heuristics] and [resolve_typeclasses].
In case of failure they raise [NoMatch] *)
val unify_HO : env -> evar_map -> constr -> constr -> evar_map
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 06:57:55 +0000