aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp')
-rw-r--r--mathcomp/field/algC.v4
-rw-r--r--mathcomp/ssreflect/eqtype.v12
-rw-r--r--mathcomp/ssreflect/plugin/trunk/ssreflect.ml439
-rw-r--r--mathcomp/ssreflect/plugin/v8.4/ssreflect.ml42
-rw-r--r--mathcomp/ssreflect/plugin/v8.5/ssreflect.ml42
-rw-r--r--mathcomp/ssreflect/plugin/v8.6/ssreflect.ml42
6 files changed, 31 insertions, 30 deletions
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index 6c53127..cbcbc3a 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -445,8 +445,8 @@ rewrite -(fmorph_root CtoL_rmorphism) -map_poly_comp; congr (root _ _): pu0.
by apply/esym/eq_map_poly; apply: fmorph_eq_rat.
Qed.
-Program Definition conjMixin :=
- ImaginaryMixin (svalP (imaginary_exists closedFieldType))
+Definition conjMixin :=
+ ImaginaryMixin (svalP (imaginary_exists closedFieldType))
(fun x => esym (normK x)).
Canonical numClosedFieldType := NumClosedFieldType type conjMixin.
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 85e531c..62a455b 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -177,8 +177,8 @@ Hint Resolve eq_refl eq_sym.
Section Contrapositives.
-Variable T : eqType.
-Implicit Types (A : pred T) (b : bool) (x : T).
+Variables (T1 T2 : eqType).
+Implicit Types (A : pred T1) (b : bool) (x : T1) (z : T2).
Lemma contraTeq b x y : (x != y -> ~~ b) -> b -> x = y.
Proof. by move=> imp hyp; apply/eqP; apply: contraTT hyp. Qed.
@@ -207,10 +207,10 @@ Proof. by move=> imp /eqP; apply: contraTF. Qed.
Lemma contra_eqT b x y : (~~ b -> x != y) -> x = y -> b.
Proof. by move=> imp /eqP; apply: contraLR. Qed.
-Lemma contra_eq x1 y1 x2 y2 : (x2 != y2 -> x1 != y1) -> x1 = y1 -> x2 = y2.
+Lemma contra_eq z1 z2 x1 x2 : (x1 != x2 -> z1 != z2) -> z1 = z2 -> x1 = x2.
Proof. by move=> imp /eqP; apply: contraTeq. Qed.
-Lemma contra_neq x1 y1 x2 y2 : (x2 = y2 -> x1 = y1) -> x1 != y1 -> x2 != y2.
+Lemma contra_neq z1 z2 x1 x2 : (x1 = x2 -> z1 = z2) -> z1 != z2 -> x1 != x2.
Proof. by move=> imp; apply: contraNneq => /imp->. Qed.
Lemma memPn A x : reflect {in A, forall y, y != x} (x \notin A).
@@ -230,8 +230,8 @@ Proof. by rewrite eq_sym; apply: ifN. Qed.
End Contrapositives.
-Implicit Arguments memPn [T A x].
-Implicit Arguments memPnC [T A x].
+Implicit Arguments memPn [T1 A x].
+Implicit Arguments memPnC [T1 A x].
Theorem eq_irrelevance (T : eqType) x y : forall e1 e2 : x = y :> T, e1 = e2.
Proof.
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index ee13c15..93a1ba7 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -29,7 +29,7 @@ open Pcoq.Prim
open Pcoq.Constr
open Genarg
open Stdarg
-open Constrarg
+open Tacarg
open Term
open Vars
open Context
@@ -45,6 +45,7 @@ open Coqlib
open Glob_term
open Util
open Evd
+open Proofview.Notations
open Sigma.Notations
open Extend
open Goptions
@@ -52,7 +53,7 @@ open Tacexpr
open Tacinterp
open Pretyping
open Constr
-open Tactic
+open Pltac
open Extraargs
open Ppconstr
open Printer
@@ -99,8 +100,8 @@ module Intset = Evar.Set
type loc = Loc.t
let dummy_loc = Loc.ghost
-let errorstrm = CErrors.errorlabstrm "ssreflect"
-let loc_error loc msg = CErrors.user_err_loc (loc, msg, str msg)
+let errorstrm msg = CErrors.user_err ~hdr:"ssreflect" msg
+let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg)
let anomaly s = CErrors.anomaly (str s)
(* Compatibility with Coq 8.6 *)
@@ -471,7 +472,7 @@ let _ =
Goptions.optwrite = (fun _ ->
Lib.add_anonymous_leaf (inVersion ssrAstVersion)) }
-let tactic_expr = Tactic.tactic_expr
+let tactic_expr = Pltac.tactic_expr
let gallina_ext = Vernac_.gallina_ext
let sprintf = Printf.sprintf
let tactic_mode = G_ltac.tactic_mode
@@ -1138,7 +1139,7 @@ let interp_view_nbimps ist gl rc =
let si = sig_it gl in
let gl = re_sig si sigma in
let pl, c = splay_open_constr gl t in
- if isAppInd gl c then List.length pl else ~-(List.length pl)
+ if isAppInd gl c then List.length pl else (-(List.length pl))
with _ -> 0
(* }}} *)
@@ -1222,7 +1223,7 @@ let interp_search_notation loc s opt_scope =
let ambig = "This string refers to a complex or ambiguous notation." in
str ambig ++ str "\nTry searching with one of\n" ++ ntns
with _ -> str "This string is not part of an identifier or notation." in
- CErrors.user_err_loc (loc, "interp_search_notation", diagnosis)
+ CErrors.user_err ~loc ~hdr:"interp_search_notation" diagnosis
let pr_ssr_search_item _ _ _ = pr_search_item
@@ -1233,7 +1234,7 @@ let is_ident s = try CLexer.check_ident s; true with _ -> false
let is_ident_part s = is_ident ("H" ^ s)
let interp_search_notation loc tag okey =
- let err msg = CErrors.user_err_loc (loc, "interp_search_notation", msg) in
+ let err msg = CErrors.user_err ~loc ~hdr:"interp_search_notation" msg in
let mk_pntn s for_key =
let n = String.length s in
let s' = String.make (n + 2) ' ' in
@@ -1454,7 +1455,7 @@ let interp_modloc mr =
let interp_mod (_, mr) =
let (loc, qid) = qualid_of_reference mr in
try Nametab.full_name_module qid with Not_found ->
- CErrors.user_err_loc (loc, "interp_modloc", str "No Module " ++ pr_qualid qid) in
+ CErrors.user_err ~loc ~hdr:"interp_modloc" (str "No Module " ++ pr_qualid qid) in
let mr_out, mr_in = List.partition fst mr in
let interp_bmod b = function
| [] -> fun _ _ _ -> true
@@ -1465,7 +1466,7 @@ let interp_modloc mr =
(* The unified, extended vernacular "Search" command *)
let ssrdisplaysearch gr env t =
- let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in
+ let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in
msg_info (hov 2 pr_res ++ fnl ())
VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY
@@ -1760,7 +1761,7 @@ let pr_ssrhyp _ _ _ = pr_hyp
let wit_ssrhyprep = add_genarg "ssrhyprep" pr_hyp
let hyp_err loc msg id =
- CErrors.user_err_loc (loc, "ssrhyp", str msg ++ pr_id id)
+ CErrors.user_err ~loc ~hdr:"ssrhyp" (str msg ++ pr_id id)
let intern_hyp ist (SsrHyp (loc, id) as hyp) =
let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) (loc, id)) in
@@ -2084,8 +2085,8 @@ let abs_wgen keep_let ist f gen (gl,args,c) =
let sigma, env = project gl, pf_env gl in
let evar_closed t p =
if occur_existential t then
- CErrors.user_err_loc (loc_of_cpattern p,"ssreflect",
- pr_constr_pat t ++
+ CErrors.user_err ~loc:(loc_of_cpattern p) ~hdr:"ssreflect"
+ (pr_constr_pat t ++
str" contains holes and matches no subterm of the goal") in
match gen with
| _, Some ((x, mode), None) when mode = "@" || (mode = " " && keep_let) ->
@@ -2689,7 +2690,7 @@ END
(* subsets of patterns *)
let check_ssrhpats loc w_binders ipats =
- let err_loc s = CErrors.user_err_loc (loc, "ssreflect", s) in
+ let err_loc s = CErrors.user_err ~loc ~hdr:"ssreflect" s in
let clr, ipats =
let rec aux clr = function
| IpatSimpl (cl, Nop) :: tl -> aux (clr @ cl) tl
@@ -5703,7 +5704,7 @@ ARGUMENT EXTEND ssrhavefwdwbinders
tr, ((((clr, pats), allbinders), simpl), hint) ]
END
-(* Tactic. *)
+(* Pltac. *)
let is_Evar_or_CastedMeta x =
isEvar_or_Meta x ||
@@ -6205,8 +6206,8 @@ END
(* longer and thus comment out. Such comments are marked with v8.3 *)
GEXTEND Gram
- GLOBAL: Tactic.hypident;
- Tactic.hypident: [
+ GLOBAL: Pltac.hypident;
+ Pltac.hypident: [
[ "("; IDENT "type"; "of"; id = Prim.identref; ")" -> id, InHypTypeOnly
| "("; IDENT "value"; "of"; id = Prim.identref; ")" -> id, InHypValueOnly
] ];
@@ -6223,8 +6224,8 @@ hloc: [
END
GEXTEND Gram
- GLOBAL: Tactic.constr_eval;
- Tactic.constr_eval: [
+ GLOBAL: Pltac.constr_eval;
+ Pltac.constr_eval: [
[ IDENT "type"; "of"; c = Constr.constr -> Genredexpr.ConstrTypeOf c ]
];
END
diff --git a/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4
index b5cd80a..3ce494f 100644
--- a/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4
@@ -1447,7 +1447,7 @@ let interp_modloc mr =
(* The unified, extended vernacular "Search" command *)
let ssrdisplaysearch gr env t =
- let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env t in
+ let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env t in
msg (hov 2 pr_res ++ fnl ())
VERNAC COMMAND EXTEND SsrSearchPattern
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
index 85a6fef..8409bfb 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
@@ -1436,7 +1436,7 @@ let interp_modloc mr =
(* The unified, extended vernacular "Search" command *)
let ssrdisplaysearch gr env t =
- let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in
+ let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in
msg_info (hov 2 pr_res ++ fnl ())
VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY
diff --git a/mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4
index 666b46e..15fc5e5 100644
--- a/mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4
@@ -1470,7 +1470,7 @@ let interp_modloc mr =
(* The unified, extended vernacular "Search" command *)
let ssrdisplaysearch gr env t =
- let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in
+ let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in
msg_info (hov 2 pr_res ++ fnl ())
VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 10:06:57 +0000