aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--etc/ANNOUNCE-github.md2
-rwxr-xr-xetc/win-installer.nsi56
-rw-r--r--mathcomp/Make1
-rw-r--r--mathcomp/algebra/intdiv.v2
-rw-r--r--mathcomp/odd_order/PFsection5.v2
-rw-r--r--mathcomp/ssreflect/Makefile.coq-makefile9
-rw-r--r--mathcomp/ssreflect/div.v6
-rw-r--r--mathcomp/ssreflect/opam2
-rw-r--r--mathcomp/ssreflect/plugin/trunk/ssreflect.ml4129
-rw-r--r--mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4110
-rw-r--r--mathcomp/ssreflect/plugin/v8.4/ssreflect.ml49
-rw-r--r--mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml417
-rw-r--r--mathcomp/ssreflect/plugin/v8.5/ssreflect.ml418
-rw-r--r--mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml454
-rw-r--r--mathcomp/ssreflect/prime.v6
-rw-r--r--mathcomp/ssreflect/ssreflect.v1
-rw-r--r--mathcomp/ssreflect/ssrnat.v4
-rw-r--r--mathcomp/ssrtest/Make1
-rw-r--r--mathcomp/ssrtest/tacnotationpattern.v14
19 files changed, 268 insertions, 175 deletions
diff --git a/etc/ANNOUNCE-github.md b/etc/ANNOUNCE-github.md
index 95f633f..79e5730 100644
--- a/etc/ANNOUNCE-github.md
+++ b/etc/ANNOUNCE-github.md
@@ -17,7 +17,7 @@ library will be carefully assessed on all the mature projects part of the organi
exchange we expect members of the organization to actively maintain their code when a breaking
change is applied or a patch is proposed.
-The organization hosts a [wiki](https://github.com/math-comp/math-comp/wiki/wiki) for exchanging tips
+The organization hosts a [wiki](https://github.com/math-comp/wiki/wiki) for exchanging tips
and tricks, gotchas, good practices, etc.
The ssreflect [mailing list](https://sympa.inria.fr/sympa/info/ssreflect) shall serve as the
diff --git a/etc/win-installer.nsi b/etc/win-installer.nsi
index 8562acc..7b08705 100755
--- a/etc/win-installer.nsi
+++ b/etc/win-installer.nsi
@@ -1,13 +1,11 @@
SetCompressor lzma
-; The VERSION should be passed as an argument at compile time using :
-; nsis -DVERSION=1.5 win-installer.nsi
+; VERSION and BITS should be passed as an argument at compile time using:
+; makensis -DVERSION=1.6 -DBITS=32 win-installer.nsi
!define MY_PRODUCT "Coq" ;Define your own software name here
-!define SRC ".\"
-!define SRC_SSR "C:\Coq\lib\user-contrib\Ssreflect\"
-!define SRC_MC "C:\Coq\lib\user-contrib\MathComp\"
-!define OUTFILE "ssr-mathcomp-installer-${VERSION}.exe"
+!define SRC "C:\coq${BITS}\lib\user-contrib\mathcomp\"
+!define OUTFILE "ssreflect-mathcomp-installer-${VERSION}-win${BITS}.exe"
!include "MUI2.nsh"
@@ -29,7 +27,7 @@ SetCompressor lzma
;Modern UI Configuration
!insertmacro MUI_PAGE_WELCOME
- !insertmacro MUI_PAGE_LICENSE "${SRC}\CeCILL-B"
+ !insertmacro MUI_PAGE_LICENSE ".\CeCILL-B"
!insertmacro MUI_PAGE_COMPONENTS
!define MUI_DIRECTORYPAGE_TEXT_TOP "Select where Coq is installed."
!insertmacro MUI_PAGE_DIRECTORY
@@ -50,27 +48,25 @@ SetCompressor lzma
;Language Strings
;Description
- LangString DESC_1 ${LANG_ENGLISH} "This package contains the Ssreflect proof language."
- LangString DESC_2 ${LANG_ENGLISH} "This package contains the Mathematical Components lirbary."
+ LangString DESC ${LANG_ENGLISH} "The Ssreflect proof language and the Mathematical Components library."
;--------------------------------
;Installer Sections
-Section "Ssreflect" Sec1
+Section "Ssreflect and MathComp" Sec
- SetOutPath "$INSTDIR\lib\user-contrib\Ssreflect\"
+ SetOutPath "$INSTDIR\lib\user-contrib\mathcomp\"
- File /r ${SRC_SSR}\*.vo
- File /r ${SRC_SSR}\*.v
- File /r ${SRC_SSR}\*.glob
- File /r ${SRC_SSR}\*.cmx
- File /r ${SRC_SSR}\*.cmxs
- File /r ${SRC_SSR}\*.cmi
+ File /r ${SRC}\*.vo
+ File /r ${SRC}\*.v
+ File /r ${SRC}\*.glob
+ File /r ${SRC}\*.cmxs
+ File /r ${SRC}\*.cmi
CreateDirectory "$SMPROGRAMS\Coq"
- WriteINIStr "$SMPROGRAMS\Coq\The Ssreflect Library.url" "InternetShortcut" "URL" "http://ssr.msr-inria.inria.fr/doc/ssreflect-${VERSION}/"
+ WriteINIStr "$SMPROGRAMS\Coq\The Mathematical Components Library.url" "InternetShortcut" "URL" "http://math-comp.github.io/math-comp/"
WriteINIStr "$SMPROGRAMS\Coq\The Ssreflect User Manaul.url" "InternetShortcut" "URL" "http://hal.inria.fr/inria-00258384/en"
@@ -79,35 +75,15 @@ Section "Ssreflect" Sec1
SectionEnd
-Section "MathComp" Sec2
-
- SetOutPath "$INSTDIR\lib\user-contrib\MathComp\"
-
- File /r ${SRC_MC}\*.vo
- File /r ${SRC_MC}\*.v
- File /r ${SRC_MC}\*.glob
- File /r ${SRC_MC}\*.cmx
- File /r ${SRC_MC}\*.cmxs
- File /r ${SRC_MC}\*.cmi
-
- CreateDirectory "$SMPROGRAMS\Coq"
-
- WriteINIStr "$SMPROGRAMS\Coq\The Mathematical Components Library.url" "InternetShortcut" "URL" "http://ssr.msr-inria.inria.fr/doc/mathcomp-${VERSION}/"
-
-SectionEnd
-
!insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN
- !insertmacro MUI_DESCRIPTION_TEXT ${Sec1} $(DESC_1)
- !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2)
+ !insertmacro MUI_DESCRIPTION_TEXT ${Sec} $(DESC)
!insertmacro MUI_FUNCTION_DESCRIPTION_END
Section "Uninstall"
- RMDir /r "$INSTDIR\lib\user-contrib\MathComp\"
- RMDir /r "$INSTDIR\lib\user-contrib\Ssreflect\"
+ RMDir /r "$INSTDIR\lib\user-contrib\mathcomp\"
Delete "$SMPROGRAMS\Coq\The Mathematical Components Library.url"
- Delete "$SMPROGRAMS\Coq\The Ssreflect Library.url"
Delete "$SMPROGRAMS\Coq\The Ssreflect User Manaul.url"
Delete "$INSTDIR\Uninstall Ssreflect and MathComp.exe"
diff --git a/mathcomp/Make b/mathcomp/Make
index 9f41de1..a235149 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -172,6 +172,7 @@ ssrtest/view_case.v
ssrtest/wlogletin.v
ssrtest/wlog_suff.v
ssrtest/wlong_intro.v
+ssrtest/tacnotationpattern.v
ssreflect.ml4
ssreflect.mllib
ssrmatching.ml4
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 2484365..2871ff5 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -164,7 +164,7 @@ Proof. by move=> p_nz /subnK{2}<-; rewrite exprD mulzK // expf_neq0. Qed.
Lemma modz1 m : (m %% 1)%Z = 0.
Proof. by case: m => n; rewrite (modNz_nat, modz_nat) ?modn1. Qed.
-Lemma divn1 m : (m %/ 1)%Z = m. Proof. by rewrite -{1}[m]mulr1 mulzK. Qed.
+Lemma divz1 m : (m %/ 1)%Z = m. Proof. by rewrite -{1}[m]mulr1 mulzK. Qed.
Lemma divzz d : (d %/ d)%Z = (d != 0).
Proof. by have [-> // | d_nz] := altP eqP; rewrite -{1}[d]mul1r mulzK. Qed.
diff --git a/mathcomp/odd_order/PFsection5.v b/mathcomp/odd_order/PFsection5.v
index b1a5a32..d318f5f 100644
--- a/mathcomp/odd_order/PFsection5.v
+++ b/mathcomp/odd_order/PFsection5.v
@@ -1286,7 +1286,7 @@ have haveX xi: xi \in S2 chi1 -> exists2 X, Xspec X & Xi_spec X xi.
- apply: sub_iso_to IZtau; last exact: zcharW.
by apply: zchar_trans_on; apply/allP; rewrite /= !Zd.
have [||minX1 _]:= subcoherent_norm _ _ (erefl _) defX1Y2.
- - rewrite char_vchar ?N_S /orthogonal //= !oSS ?eqxx ?inv_eq //.
+ - rewrite char_vchar ?N_S /orthogonal //= !oSS ?eqxx // inv_eq //.
exact: cfConjCK.
- apply: sub_iso_to IZtau; last exact: zcharW.
by apply: zchar_trans_on; apply/allP; rewrite /= !Zd.
diff --git a/mathcomp/ssreflect/Makefile.coq-makefile b/mathcomp/ssreflect/Makefile.coq-makefile
index 9cce300..52beace 100644
--- a/mathcomp/ssreflect/Makefile.coq-makefile
+++ b/mathcomp/ssreflect/Makefile.coq-makefile
@@ -1,9 +1,10 @@
define coqmakefile
(echo "Generating Makefile.coq for Coq $(V) with COQBIN=$(COQBIN)";\
- ln -sf $(1)/plugin/$(V)/ssreflect.mllib .;\
- ln -sf $(1)/plugin/$(V)/ssrmatching.mli .;\
- ln -sf $(1)/plugin/$(V)/ssrmatching.ml4 .;\
- ln -sf $(1)/plugin/$(V)/ssreflect.ml4 .;\
+ if [ "$$OS" = "Windows_NT" ]; then LN=cp; else LN="ln -sf"; fi;\
+ $$LN $(1)/plugin/$(V)/ssreflect.mllib .;\
+ $$LN $(1)/plugin/$(V)/ssrmatching.mli .;\
+ $$LN $(1)/plugin/$(V)/ssrmatching.ml4 .;\
+ $$LN $(1)/plugin/$(V)/ssreflect.ml4 .;\
$(COQBIN)coq_makefile -f Make -o Makefile.coq)
endef
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index e858d54..8179f57 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -457,6 +457,12 @@ Qed.
Lemma dvdn_exp k d m : 0 < k -> d %| m -> d %| (m ^ k).
Proof. by case: k => // k _ d_dv_m; rewrite expnS dvdn_mulr. Qed.
+Lemma dvdn_fact m n : 0 < m <= n -> m %| n`!.
+Proof.
+case: m => //= m; elim: n => //= n IHn; rewrite ltnS leq_eqVlt.
+by case/predU1P=> [-> | /IHn]; [apply: dvdn_mulr | apply: dvdn_mull].
+Qed.
+
Hint Resolve dvdn_add dvdn_sub dvdn_exp.
Lemma eqn_mod_dvd d m n : n <= m -> (m == n %[mod d]) = (d %| m - n).
diff --git a/mathcomp/ssreflect/opam b/mathcomp/ssreflect/opam
index 2f6fbdf..1601e89 100644
--- a/mathcomp/ssreflect/opam
+++ b/mathcomp/ssreflect/opam
@@ -10,7 +10,7 @@ license: "CeCILL-B"
build: [ make "-j" "%{jobs}%" ]
install: [ make "install" ]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp'" ]
-depends: [ "coq" { ( >= "8.4pl4" & < "8.5" ) | ( = "8.5.dev" ) | ( = "dev")} ]
+depends: [ "coq" { ((>= "8.4pl4" & < "8.5~") | (>= "8.5" & < "8.6~") | (= "dev"))} ]
tags: [ "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ]
authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ]
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index f3a4f70..d6a5175 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -3,17 +3,14 @@
(* This line is read by the Makefile's dist target: do not remove. *)
DECLARE PLUGIN "ssreflect"
-let ssrversion = "1.5";;
+let ssrversion = "1.6";;
let ssrAstVersion = 1;;
let () = Mltop.add_known_plugin (fun () ->
if Flags.is_verbose () && not !Flags.batch_mode then begin
Printf.printf "\nSmall Scale Reflection version %s loaded.\n" ssrversion;
Printf.printf "Copyright 2005-2014 Microsoft Corporation and INRIA.\n";
Printf.printf "Distributed under the terms of the CeCILL-B license.\n\n"
- end;
- (* Disable any semantics associated with bullets *)
- Goptions.set_string_option_value_gen
- (Some false) ["Bullet";"Behavior"] "None")
+ end)
"ssreflect"
;;
@@ -112,10 +109,12 @@ let mkSsrRef name =
Errors.error "Small scale reflection library not loaded"
let mkSsrRRef name = GRef (dummy_loc, mkSsrRef name,None), None
let mkSsrConst name env sigma =
- Evd.fresh_global env sigma (mkSsrRef name)
+ Sigma.fresh_global env sigma (mkSsrRef name)
let pf_mkSsrConst name gl =
let sigma, env, it = project gl, pf_env gl, sig_it gl in
- let sigma, t = mkSsrConst name env sigma in
+ let sigma = Sigma.Unsafe.of_evar_map sigma in
+ let Sigma (t, sigma, _) = mkSsrConst name env sigma in
+ let sigma = Sigma.to_evar_map sigma in
t, re_sig it sigma
let pf_fresh_global name gl =
let sigma, env, it = project gl, pf_env gl, sig_it gl in
@@ -210,7 +209,7 @@ let add_genarg tag pr =
let wit = Genarg.make0 None tag in
let glob ist x = (ist, x) in
let subst _ x = x in
- let interp ist gl x = (gl.Evd.sigma, x) in
+ let interp ist x = Ftactic.return x in
let gen_pr _ _ _ = pr in
let () = Genintern.register_intern0 wit glob in
let () = Genintern.register_subst0 wit subst in
@@ -478,7 +477,7 @@ let _ =
Goptions.optdepr = false;
Goptions.optwrite = (fun b -> ssroldreworder := b) }
-let ssrhaveNOtcresolution = ref false
+let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false
let inHaveTCResolution = Libobject.declare_object {
(Libobject.default_object "SSRHAVETCRESOLUTION") with
@@ -554,7 +553,7 @@ let is_pf_var c = isVar c && not_section_id (destVar c)
let pf_ids_of_proof_hyps gl =
let add_hyp (id, _, _) ids = if not_section_id id then id :: ids else ids in
- Context.fold_named_context add_hyp (pf_hyps gl) ~init:[]
+ Context.Named.fold_outside add_hyp (pf_hyps gl) ~init:[]
let pf_nf_evar gl e = Reductionops.nf_evar (project gl) e
@@ -583,6 +582,7 @@ let basecuttac name c gl =
let t = mkApp (hd, [|c|]) in
let gl, _ = pf_e_type_of gl t in
Proofview.V82.of_tactic (apply t) gl
+let apply_type x xs = Proofview.V82.of_tactic (apply_type x xs)
(* we reduce head beta redexes *)
let betared env =
@@ -796,7 +796,7 @@ let pf_abs_evars gl (sigma, c0) =
let abs_dc c = function
| x, Some b, t -> mkNamedLetIn x b t (mkArrow t c)
| x, None, t -> mkNamedProd x t c in
- let t = Context.fold_named_context_reverse abs_dc ~init:evi.evar_concl dc in
+ let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in
Evarutil.nf_evar sigma t in
let rec put evlist c = match kind_of_term c with
| Evar (k, a) ->
@@ -851,7 +851,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
let abs_dc c = function
| x, Some b, t -> mkNamedLetIn x b t (mkArrow t c)
| x, None, t -> mkNamedProd x t c in
- let t = Context.fold_named_context_reverse abs_dc ~init:evi.evar_concl dc in
+ let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in
Evarutil.nf_evar sigma0 (Evarutil.nf_evar sigma t) in
let rec put evlist c = match kind_of_term c with
| Evar (k, a) ->
@@ -1027,16 +1027,14 @@ let ssrtac_entry name n = {
}
let set_pr_ssrtac name prec afmt =
- let fmt = List.map (function ArgSep s -> Some s | _ -> None) afmt in
- let rec mk_akey = function
- | ArgSsr s :: afmt' -> ExtraArgType ("ssr" ^ s) :: mk_akey afmt'
- | ArgCoq a :: afmt' -> a :: mk_akey afmt'
- | ArgSep _ :: afmt' -> mk_akey afmt'
- | [] -> [] in
+ let fmt = List.map (function
+ | ArgSep s -> Egramml.GramTerminal s
+ | ArgSsr s -> Egramml.GramTerminal s
+ | ArgCoq at -> Egramml.GramTerminal "COQ_ARG") afmt in
let tacname = ssrtac_name name in
Pptactic.declare_ml_tactic_pprule tacname [|
- { Pptactic.pptac_args = mk_akey afmt;
- Pptactic.pptac_prods = (prec, fmt) }
+ { Pptactic.pptac_level = prec;
+ Pptactic.pptac_prods = fmt }
|]
let ssrtac_atom loc name args = TacML (loc, ssrtac_entry name 0, args)
@@ -1051,18 +1049,30 @@ let ssrevaltac ist gtac =
(** Generic argument-based globbing/typing utilities *)
+let of_ftactic ftac gl =
+ let r = ref None in
+ let tac = Ftactic.run ftac (fun ans -> r := Some ans; Proofview.tclUNIT ()) in
+ let tac = Proofview.V82.of_tactic tac in
+ let { sigma = sigma } = tac gl in
+ let ans = match !r with
+ | None -> assert false (** If the tactic failed we should not reach this point *)
+ | Some ans -> ans
+ in
+ (sigma, ans)
let interp_wit wit ist gl x =
let globarg = in_gen (glbwit wit) x in
- let sigma, arg = interp_genarg ist (pf_env gl) (project gl) (pf_concl gl) gl.Evd.it globarg in
- sigma, out_gen (topwit wit) arg
+ let arg = interp_genarg ist globarg in
+ let (sigma, arg) = of_ftactic arg gl in
+ sigma, Value.cast (topwit wit) arg
let interp_intro_pattern = interp_wit wit_intro_pattern
let interp_constr = interp_wit wit_constr
let interp_open_constr ist gl gc =
- interp_wit wit_open_constr ist gl ((), gc)
+ let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, NoBindings) in
+ (project gl, (sigma, c))
let interp_refine ist gl rc =
let constrvars = extract_ltac_constr_values ist (pf_env gl) in
@@ -1446,7 +1456,7 @@ let interp_modloc mr =
let ssrdisplaysearch gr env t =
let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in
- msg (hov 2 pr_res ++ fnl ())
+ msg_info (hov 2 pr_res ++ fnl ())
VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY
| [ "Search" ssr_search_arg(a) ssr_modlocs(mr) ] ->
@@ -1496,6 +1506,7 @@ let mk_rtype t = Some t in
let mk_dthen loc (mp, ct, rt) c = (loc, mp, c), ct, rt in
let mk_let loc rt ct mp c1 =
CCases (loc, LetPatternStyle, rt, ct, [loc, mp, c1]) in
+let mk_pat c (na, t) = (c, na, t) in
GEXTEND Gram
GLOBAL: binder_constr;
ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> mk_rtype t ]];
@@ -1510,20 +1521,20 @@ GEXTEND Gram
ssr_else: [[ mp = ssr_elsepat; c = lconstr -> !@loc, mp, c ]];
binder_constr: [
[ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
- let b1, ct, rt = db1 in CCases (!@loc, MatchStyle, rt, [c, ct], [b1; b2])
+ let b1, ct, rt = db1 in CCases (!@loc, MatchStyle, rt, [mk_pat c ct], [b1; b2])
| "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->
let b1, ct, rt = db1 in
let b1, b2 =
let (l1, p1, r1), (l2, p2, r2) = b1, b2 in (l1, p1, r2), (l2, p2, r1) in
- CCases (!@loc, MatchStyle, rt, [c, ct], [b1; b2])
+ CCases (!@loc, MatchStyle, rt, [mk_pat c ct], [b1; b2])
| "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr ->
- mk_let (!@loc) no_rt [c, no_ct] mp c1
+ mk_let (!@loc) no_rt [mk_pat c no_ct] mp c1
| "let"; ":"; mp = ssr_mpat; ":="; c = lconstr;
rt = ssr_rtype; "in"; c1 = lconstr ->
- mk_let (!@loc) rt [c, mk_cnotype mp] mp c1
+ mk_let (!@loc) rt [mk_pat c (mk_cnotype mp)] mp c1
| "let"; ":"; mp = ssr_mpat; "in"; t = pattern; ":="; c = lconstr;
rt = ssr_rtype; "in"; c1 = lconstr ->
- mk_let (!@loc) rt [c, mk_ctype mp t] mp c1
+ mk_let (!@loc) rt [mk_pat c (mk_ctype mp t)] mp c1
] ];
END
@@ -1683,7 +1694,7 @@ TACTIC EXTEND ssrtclstar
END
set_pr_ssrtac "tclstar" 5 [ArgSep "- "; ArgSsr "tclarg"]
-let gen_tclarg = in_gen (rawwit wit_ssrtclarg)
+let gen_tclarg tac = TacGeneric (in_gen (rawwit wit_ssrtclarg) tac)
GEXTEND Gram
GLOBAL: tactic tactic_mode;
@@ -1722,7 +1733,7 @@ GEXTEND Gram
ssrhint: [[ "by"; arg = ssrhintarg -> arg ]];
simple_tactic: [
[ "by"; arg = ssrhintarg ->
- let garg = in_gen (rawwit wit_ssrhint) arg in
+ let garg = TacGeneric (in_gen (rawwit wit_ssrhint) arg) in
ssrtac_atom !@loc "tclby" [garg]
] ];
END
@@ -1808,7 +1819,7 @@ let rec check_hyps_uniq ids = function
| [] -> ()
let check_hyp_exists hyps (SsrHyp(_, id)) =
- try ignore(Context.lookup_named id hyps)
+ try ignore(Context.Named.lookup id hyps)
with Not_found -> errorstrm (str"No assumption is named " ++ pr_id id)
let interp_hyps ist gl ghyps =
@@ -2044,7 +2055,7 @@ let endclausestac id_map clseq gl_id cl0 gl =
| _ -> map_constr unmark c in
let utac hyp =
Proofview.V82.of_tactic
- (convert_hyp_no_check (map_named_declaration unmark hyp)) in
+ (convert_hyp_no_check (Context.Named.Declaration.map unmark hyp)) in
let utacs = List.map utac (pf_hyps gl) in
let ugtac gl' =
Proofview.V82.of_tactic
@@ -2226,7 +2237,7 @@ let interp_index ist gl idx =
with _ -> loc_error loc "Index not a number" in
ArgArg (check_index loc i)
-ARGUMENT EXTEND ssrindex TYPED AS int_or_var PRINTED BY pr_ssrindex
+ARGUMENT EXTEND ssrindex TYPED AS ssrindex PRINTED BY pr_ssrindex
INTERPRETED BY interp_index
| [ int_or_var(i) ] -> [ mk_index loc i ]
END
@@ -2498,10 +2509,13 @@ let remove_loc = snd
let rec ipat_of_intro_pattern = function
| IntroNaming (IntroIdentifier id) -> IpatId id
| IntroAction IntroWildcard -> IpatWild
- | IntroAction (IntroOrAndPattern iorpat) ->
+ | IntroAction (IntroOrAndPattern (IntroOrPattern iorpat)) ->
IpatCase
(List.map (List.map ipat_of_intro_pattern)
(List.map (List.map remove_loc) iorpat))
+ | IntroAction (IntroOrAndPattern (IntroAndPattern iandpat)) ->
+ IpatCase
+ [List.map ipat_of_intro_pattern (List.map remove_loc iandpat)]
| IntroNaming IntroAnonymous -> IpatAnon
| IntroAction (IntroRewrite b) -> IpatRw (allocc, if b then L2R else R2L)
| IntroNaming (IntroFresh id) -> IpatAnon
@@ -2549,8 +2563,10 @@ let rec add_intro_pattern_hyps (loc, ipat) hyps = match ipat with
if not_section_id id then SsrHyp (loc, id) :: hyps else
hyp_err loc "Can't delete section hypothesis " id
| IntroAction IntroWildcard -> hyps
- | IntroAction (IntroOrAndPattern iorpat) ->
+ | IntroAction (IntroOrAndPattern (IntroOrPattern iorpat)) ->
List.fold_right (List.fold_right add_intro_pattern_hyps) iorpat hyps
+ | IntroAction (IntroOrAndPattern (IntroAndPattern iandpat)) ->
+ List.fold_right add_intro_pattern_hyps iandpat hyps
| IntroNaming IntroAnonymous -> []
| IntroNaming (IntroFresh _) -> []
| IntroAction (IntroRewrite _) -> hyps
@@ -2836,7 +2852,7 @@ let clear_with_wilds wilds clr0 gl =
let vars = global_vars_set_of_decl (pf_env gl) nd in
let occurs id' = Idset.mem id' vars in
if List.exists occurs clr then id :: clr else clr in
- clear (Context.fold_named_context_reverse extend_clr ~init:clr0 (pf_hyps gl)) gl
+ clear (Context.Named.fold_inside extend_clr ~init:clr0 (pf_hyps gl)) gl
let tclTHENS_nonstrict tac tacl taclname gl =
let tacres = tac gl in
@@ -2875,23 +2891,17 @@ let mk_abstract_id () = incr ssr_abstract_id; nat_of_n !ssr_abstract_id
let ssrmkabs id gl =
let env, concl = pf_env gl, pf_concl gl in
let step = { run = begin fun sigma ->
- let sigma = Sigma.to_evar_map sigma in
- let sigma, abstract_proof, abstract_ty =
- let sigma, (ty, _) =
+ let Sigma ((abstract_proof, abstract_ty), sigma, p) =
+ let Sigma ((ty, _), sigma, p1) =
Evarutil.new_type_evar env sigma Evd.univ_flexible_alg in
- let sigma, ablock = mkSsrConst "abstract_lock" env sigma in
- let sigma = Sigma.Unsafe.of_evar_map sigma in
- let Sigma (lock, sigma, _) = Evarutil.new_evar env sigma ablock in
- let sigma = Sigma.to_evar_map sigma in
- let sigma, abstract = mkSsrConst "abstract" env sigma in
+ let Sigma (ablock, sigma, p2) = mkSsrConst "abstract_lock" env sigma in
+ let Sigma (lock, sigma, p3) = Evarutil.new_evar env sigma ablock in
+ let Sigma (abstract, sigma, p4) = mkSsrConst "abstract" env sigma in
let abstract_ty = mkApp(abstract, [|ty;mk_abstract_id ();lock|]) in
- let sigma = Sigma.Unsafe.of_evar_map sigma in
- let Sigma (m, sigma, _) = Evarutil.new_evar env sigma abstract_ty in
- let sigma = Sigma.to_evar_map sigma in
- sigma, m, abstract_ty in
+ let Sigma (m, sigma, p5) = Evarutil.new_evar env sigma abstract_ty in
+ Sigma ((m, abstract_ty), sigma, p1 +> p2 +> p3 +> p4 +> p5) in
let sigma, kont =
let rd = Name id, None, abstract_ty in
- let sigma = Sigma.Unsafe.of_evar_map sigma in
let Sigma (ev, sigma, _) = Evarutil.new_evar (Environ.push_rel rd env) sigma concl in
let sigma = Sigma.to_evar_map sigma in
(sigma, ev)
@@ -3025,7 +3035,7 @@ END
set_pr_ssrtac "tclintros" 0 [ArgSsr "introsarg"]
let tclintros_expr loc tac ipats =
- let args = [in_gen (rawwit wit_ssrintrosarg) (tac, ipats)] in
+ let args = [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in
ssrtac_expr loc "tclintros" args
GEXTEND Gram
@@ -3112,7 +3122,7 @@ set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"]
let ssrdotac_expr loc n m tac clauses =
let arg = ((n, m), tac), clauses in
- ssrtac_expr loc "tcldo" [in_gen (rawwit wit_ssrdoarg) arg]
+ ssrtac_expr loc "tcldo" [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrdoarg) arg)]
GEXTEND Gram
GLOBAL: tactic_expr;
@@ -3279,7 +3289,7 @@ let tclseq_expr loc tac dir arg =
let arg1 = in_gen (rawwit wit_ssrtclarg) tac in
let arg2 = in_gen (rawwit wit_ssrseqdir) dir in
let arg3 = in_gen (rawwit wit_ssrseqarg) (check_seqtacarg dir arg) in
- ssrtac_expr loc "tclseq" [arg1; arg2; arg3]
+ ssrtac_expr loc "tclseq" (List.map (fun x -> Tacexpr.TacGeneric x) [arg1; arg2; arg3])
GEXTEND Gram
GLOBAL: tactic_expr;
@@ -3776,7 +3786,7 @@ let analyze_eliminator elimty env sigma =
str"A (applied) bound variable was expected as the conclusion of "++
str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_constr elimty) in
let ctx, pred_id, elim_is_dep, n_pred_args = loop [] elimty in
- let n_elim_args = rel_context_nhyps ctx in
+ let n_elim_args = Context.Rel.nhyps ctx in
let is_rec_elim =
let count_occurn n term =
let count = ref 0 in
@@ -3862,7 +3872,8 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
(mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n)))
in
pp(lazy(str"after: " ++ pr_constr oc));
- try applyn ~with_evars ~with_shelve:true ?beta n oc gl with _ -> raise dependent_apply_error
+ try applyn ~with_evars ~with_shelve:true ?beta n oc gl
+ with e when Errors.noncritical e -> raise dependent_apply_error
let pf_fresh_inductive_instance ind gl =
let sigma, env, it = project gl, pf_env gl, sig_it gl in
@@ -3977,7 +3988,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
let pred_id,n_elim_args,is_rec,elim_is_dep,n_pred_args =
analyze_eliminator elimty env (project gl) in
let rctx = fst (decompose_prod_assum unfolded_c_ty) in
- let n_c_args = rel_context_length rctx in
+ let n_c_args = Context.Rel.length rctx in
let c, c_ty, t_args, gl = pf_saturate gl c ~ty:c_ty n_c_args in
let elim, elimty, elim_args, gl =
pf_saturate ~beta:is_case gl elim ~ty:elimty n_elim_args in
@@ -4155,7 +4166,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
let pat = List.find (fun t -> Intset.mem i (evars_of_term t)) patterns in
errorstrm(str"Pattern"++spc()++pr_constr_pat pat++spc()++
str"was not completely instantiated and one of its variables"++spc()++
- str"occurs in the type of another non instantieted pattern variable");
+ str"occurs in the type of another non-instantiated pattern variable");
end
in
(* the elim tactic, with the eliminator and the predicated we computed *)
@@ -4951,7 +4962,7 @@ let rwprocess_rule dir rule gl =
let t =
if red = 1 then Tacred.hnf_constr env sigma t0
else Reductionops.whd_betaiotazeta sigma t0 in
- pp(lazy(str"rewrule="++pr_constr t));
+ pp(lazy(str"rewrule="++pr_constr_pat t));
match kind_of_term t with
| Prod (_, xt, at) ->
let sigma = create_evar_defs sigma in
@@ -5907,7 +5918,7 @@ GEXTEND Gram
tactic_expr: LEVEL "3"
[ RIGHTA [ IDENT "abstract"; gens = ssrdgens ->
ssrtac_expr !@loc "abstract"
- [Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens] ]];
+ [Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] ]];
END
TACTIC EXTEND ssrabstract
| [ "abstract" ssrdgens(gens) ] -> [
diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
index 39f3e7d..6416f85 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
@@ -30,6 +30,7 @@ open Evd
open Extend
open Goptions
open Tacexpr
+open Proofview.Notations
open Tacinterp
open Pretyping
open Constr
@@ -124,7 +125,7 @@ let add_genarg tag pr =
let wit = Genarg.make0 None tag in
let glob ist x = (ist, x) in
let subst _ x = x in
- let interp ist gl x = (gl.Evd.sigma, x) in
+ let interp ist x = Ftactic.return x in
let gen_pr _ _ _ = pr in
let () = Genintern.register_intern0 wit glob in
let () = Genintern.register_subst0 wit subst in
@@ -272,7 +273,7 @@ exception NoProgress
(* comparison can be much faster than the HO one. *)
let unif_EQ env sigma p c =
- let evars = existential_opt_value sigma in
+ let evars = existential_opt_value sigma, Evd.universes sigma in
try let _ = Reduction.conv env p ~evars c in true with _ -> false
let unif_EQ_args env sigma pa a =
@@ -345,6 +346,7 @@ let unif_end env sigma0 ise0 pt ok =
let ise = Evarconv.consider_remaining_unif_problems 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
let ise2 = Typeclasses.resolve_typeclasses ~fail:true env ise1 in
if not (ok ise) then raise NoProgress else
if ise2 == ise1 then (s, uc, t)
@@ -449,10 +451,12 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 =
let evi = Evd.find !sigma k in
let dc = List.firstn (max 0 (Array.length a - nenv)) (evar_filtered_context evi) in
let abs_dc (d, c) = function
- | x, Some b, t -> d, mkNamedLetIn x (put b) (put t) c
- | x, None, t -> mkVar x :: d, mkNamedProd x (put t) c in
+ | Context.Named.Declaration.LocalDef (x, b, t) ->
+ d, mkNamedLetIn x (put b) (put t) c
+ | Context.Named.Declaration.LocalAssum (x, t) ->
+ mkVar x :: d, mkNamedProd x (put t) c in
let a, t =
- Context.fold_named_context_reverse abs_dc ~init:([], (put evi.evar_concl)) dc in
+ Context.Named.fold_inside abs_dc ~init:([], (put evi.evar_concl)) dc in
let m = Evarutil.new_meta () in
ise := meta_declare m t !ise;
sigma := Evd.define k (applist (mkMeta m, a)) !sigma;
@@ -569,6 +573,12 @@ exception FoundUnif of (evar_map * evar_universe_context * tpattern)
(* Note: we don't update env as we descend into the term, as the primitive *)
(* unification procedure always rejects subterms with bound variables. *)
+let dont_impact_evars_in cl =
+ let evs_in_cl = Evd.evars_of_term cl in
+ fun sigma -> Evar.Set.for_all (fun k ->
+ try let _ = Evd.find_undefined sigma k in true
+ with Not_found -> false) evs_in_cl
+
(* We are forced to duplicate code between the FO/HO matching because we *)
(* have to work around several kludges in unify.ml: *)
(* - w_unify drops into second-order unification when the pattern is an *)
@@ -577,7 +587,8 @@ exception FoundUnif of (evar_map * evar_universe_context * tpattern)
(* head is an evar or meta (e.g., it fails on ?1 = nat when ?1 : Type). *)
(* - w_unify expands let-in (zeta conversion) eagerly, whereas we want to *)
(* match a head let rigidly. *)
-let match_upats_FO upats env sigma0 ise =
+let match_upats_FO upats env sigma0 ise orig_c =
+ let dont_impact_evars = dont_impact_evars_in orig_c in
let rec loop c =
let f, a = splay_app ise c in let i0 = ref (-1) in
let fpats =
@@ -608,13 +619,13 @@ let match_upats_FO upats env sigma0 ise =
let lhs = mkSubApp f i a in
let pt' = unif_end env sigma0 ise' u.up_t (u.up_ok lhs) in
raise (FoundUnif (ungen_upat lhs pt' u))
- with FoundUnif _ as sigma_u -> raise sigma_u
+ with FoundUnif (s,_,_) as sig_u when dont_impact_evars s -> raise sig_u
| Not_found -> Errors.anomaly (str"incomplete ise in match_upats_FO")
| _ -> () in
List.iter one_match fpats
done;
iter_constr_LR loop f; Array.iter loop a in
- fun c -> try loop c with Invalid_argument _ -> Errors.anomaly (str"IN FO")
+ try loop orig_c with Invalid_argument _ -> Errors.anomaly (str"IN FO")
let prof_FO = mk_profiler "match_upats_FO";;
let match_upats_FO upats env sigma0 ise c =
@@ -623,7 +634,9 @@ let match_upats_FO upats env sigma0 ise c =
let match_upats_HO ~on_instance upats env sigma0 ise c =
+ let dont_impact_evars = dont_impact_evars_in c in
let it_did_match = ref false in
+ let failed_because_of_TC = ref false in
let rec aux upats env sigma0 ise c =
let f, a = splay_app ise c in let i0 = ref (-1) in
let fpats = List.fold_right (filter_upat i0 f (Array.length a)) upats [] in
@@ -644,7 +657,9 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
let x, v, t, b = destLetIn f in
let _, pv, _, pb = destLetIn u.up_f in
let ise' = unif_HO env ise pv v in
- unif_HO (Environ.push_rel (x, None, t) env) ise' pb b
+ unif_HO
+ (Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, t)) env)
+ ise' pb b
| KpatFlex | KpatProj _ ->
unif_HO env ise u.up_f (mkSubApp f (i - Array.length u.up_a) a)
| _ -> unif_HO env ise u.up_f f in
@@ -652,16 +667,20 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
let lhs = mkSubApp f i a in
let pt' = unif_end env sigma0 ise'' u.up_t (u.up_ok lhs) in
on_instance (ungen_upat lhs pt' u)
- with FoundUnif _ as sigma_u -> raise sigma_u
+ with FoundUnif (s,_,_) as sig_u when dont_impact_evars s -> raise sig_u
| NoProgress -> it_did_match := true
- | _ -> () in
+ | Pretype_errors.PretypeError
+ (_,_,Pretype_errors.UnsatisfiableConstraints _) ->
+ failed_because_of_TC:=true
+ | e when Errors.noncritical e -> () in
List.iter one_match fpats
done;
iter_constr_LR (aux upats env sigma0 ise) f;
Array.iter (aux upats env sigma0 ise) a
in
aux upats env sigma0 ise c;
- if !it_did_match then raise NoProgress
+ if !it_did_match then raise NoProgress;
+ !failed_because_of_TC
let prof_HO = mk_profiler "match_upats_HO";;
let match_upats_HO ~on_instance upats env sigma0 ise c =
@@ -715,7 +734,8 @@ let mk_tpattern_matcher ?(all_instances=false)
match u.up_k with
| KpatLet ->
let x, pv, t, pb = destLetIn u.up_f in
- let env' = Environ.push_rel (x, None, t) env in
+ let env' =
+ Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, t)) env in
let match_let f = match kind_of_term f with
| LetIn (_, v, _, b) -> unif_EQ env sigma pv v && unif_EQ env' sigma pb b
| _ -> false in match_let
@@ -759,15 +779,19 @@ let rec uniquize = function
((fun env c h ~k ->
do_once upat_that_matched (fun () ->
+ let failed_because_of_TC = ref false in
try
if not all_instances then match_upats_FO upats env sigma0 ise c;
- match_upats_HO ~on_instance upats env sigma0 ise c;
+ failed_because_of_TC:=match_upats_HO ~on_instance upats env sigma0 ise c;
raise NoMatch
with FoundUnif sigma_u -> 0,[sigma_u]
| (NoMatch|NoProgress) when all_instances && instances () <> [] ->
0, uniquize (instances ())
| NoMatch when (not raise_NoMatch) ->
- errorstrm (source () ++ str "does not match any subterm of the goal")
+ if !failed_because_of_TC then
+ errorstrm (source ()++strbrk"matches but type classes inference fails")
+ else
+ errorstrm (source () ++ str "does not match any subterm of the goal")
| NoProgress when (not raise_NoMatch) ->
let dir = match upats_origin with Some (d,_) -> d | _ ->
Errors.anomaly (str"mk_tpattern_matcher with no upats_origin") in
@@ -791,7 +815,13 @@ let rec uniquize = function
mkApp (f', Array.map_left (subst_loop acc) a2)
else
(* TASSI: clear letin values to avoid unfolding *)
- let inc_h (n,_,ty) (env,h') = Environ.push_rel (n,None,ty) env, h' + 1 in
+ let inc_h rd (env,h') =
+ let ctx_item =
+ match rd with
+ | Context.Rel.Declaration.LocalAssum _ as x -> x
+ | Context.Rel.Declaration.LocalDef (x,_,y) ->
+ Context.Rel.Declaration.LocalAssum(x,y) in
+ Environ.push_rel ctx_item env, h' + 1 in
let f' = map_constr_with_binders_left_to_right inc_h subst_loop acc f in
mkApp (f', Array.map_left (subst_loop acc) a) in
subst_loop (env,h) c) : find_P),
@@ -894,15 +924,27 @@ let id_of_Cterm t = match id_of_cpattern t with
| Some x -> x
| None -> loc_error (loc_of_cpattern t) "Only identifiers are allowed here"
+let of_ftactic ftac gl =
+ let r = ref None in
+ let tac = Ftactic.run ftac (fun ans -> r := Some ans; Proofview.tclUNIT ()) in
+ let tac = Proofview.V82.of_tactic tac in
+ let { sigma = sigma } = tac gl in
+ let ans = match !r with
+ | None -> assert false (** If the tactic failed we should not reach this point *)
+ | Some ans -> ans
+ in
+ (sigma, ans)
+
let interp_wit wit ist gl x =
let globarg = in_gen (glbwit wit) x in
- let sigma, arg = interp_genarg ist (pf_env gl) (project gl) (pf_concl gl) gl.Evd.it globarg in
- sigma, out_gen (topwit wit) arg
+ let arg = interp_genarg ist globarg in
+ let (sigma, arg) = of_ftactic arg gl in
+ sigma, Value.cast (topwit wit) arg
let interp_constr = interp_wit wit_constr
let interp_open_constr ist gl gc =
- interp_wit wit_open_constr ist gl ((), gc)
+ interp_wit wit_open_constr ist gl gc
let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c
-let interp_term ist gl (_, c) = snd (interp_open_constr ist gl c)
+let interp_term ist gl (_, c) = (interp_open_constr ist gl c)
let glob_ssrterm gs = function
| k, (_, Some c) -> k, Tacintern.intern_constr gs c
| ct -> ct
@@ -1004,14 +1046,14 @@ let interp_pattern ist gl red redty =
let h_k = match kind_of_term h with Evar (k,_) -> k | _ -> assert false in
let to_clean, update = (* handle rename if x is already used *)
let ctx = pf_hyps gl in
- let len = Context.named_context_length ctx in
+ let len = Context.Named.length ctx in
let name = ref None in
- try ignore(Context.lookup_named x ctx); (name, fun k ->
+ try ignore(Context.Named.lookup x ctx); (name, fun k ->
if !name = None then
let nctx = Evd.evar_context (Evd.find sigma k) in
- let nlen = Context.named_context_length nctx in
+ let nlen = Context.Named.length nctx in
if nlen > len then begin
- name := Some (pi1 (List.nth nctx (nlen - len - 1)))
+ name := Some (Context.Named.Declaration.get_id (List.nth nctx (nlen - len - 1)))
end)
with Not_found -> ref (Some x), fun _ -> () in
let sigma0 = project gl in
@@ -1267,12 +1309,24 @@ let ssrpatterntac ist arg gl =
let (t, uc), concl_x =
fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in
let gl, tty = pf_type_of gl t in
- let concl = mkLetIn (Name (id_of_string "toto"), t, tty, concl_x) in
+ let concl = mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in
Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl
-TACTIC EXTEND ssrat
-| [ "ssrpattern" ssrpatternarg(arg) ] -> [ Proofview.V82.tactic (ssrpatterntac ist arg) ]
-END
+(* Register "ssrpattern" tactic *)
+let () =
+ let mltac _ ist =
+ let arg =
+ let v = Id.Map.find (Names.Id.of_string "ssrpatternarg") ist.lfun in
+ Value.cast (topwit wit_ssrpatternarg) v in
+ Proofview.V82.tactic (ssrpatterntac ist arg) in
+ let name = { mltac_plugin = "ssrmatching"; mltac_tactic = "ssrpattern"; } in
+ let () = Tacenv.register_ml_tactic name [|mltac|] in
+ let tac =
+ TacFun ([Some (Id.of_string "ssrpatternarg")],
+ TacML (Loc.ghost, { mltac_name = name; mltac_index = 0 }, [])) in
+ let obj () =
+ Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in
+ Mltop.declare_cache_obj obj "ssreflect"
let ssrinstancesof ist arg gl =
let ok rhs lhs ise = true in
diff --git a/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4
index db1f8d2..23b4ae5 100644
--- a/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4
@@ -2,17 +2,14 @@
(* Distributed under the terms of CeCILL-B. *)
(* This line is read by the Makefile's dist target: do not remove. *)
-let ssrversion = "1.5";;
+let ssrversion = "1.6";;
let ssrAstVersion = 1;;
let () = Mltop.add_known_plugin (fun () ->
if Flags.is_verbose () && not !Flags.batch_mode then begin
Printf.printf "\nSmall Scale Reflection version %s loaded.\n" ssrversion;
Printf.printf "Copyright 2005-2012 Microsoft Corporation and INRIA.\n";
Printf.printf "Distributed under the terms of the CeCILL-B license.\n\n"
- end;
- (* Disable any semantics associated with bullets *)
- Goptions.set_string_option_value_gen
- (Some false) ["Bullet";"Behavior"] "None")
+ end)
"ssreflect"
;;
(* Defining grammar rules with "xx" in it automatically declares keywords too *)
@@ -4049,7 +4046,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
let pat = List.find (fun t -> Intset.mem i (evars_of_term t)) patterns in
errorstrm(str"Pattern"++spc()++pr_constr_pat pat++spc()++
str"was not completely instantiated and one of its variables"++spc()++
- str"occurs in the type of another non instantieted pattern variable");
+ str"occurs in the type of another non-instantiated pattern variable");
end
in
(* the elim tactic, with the eliminator and the predicated we computed *)
diff --git a/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4
index c55067c..08f1780 100644
--- a/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/v8.4/ssrmatching.ml4
@@ -590,6 +590,7 @@ let match_upats_FO upats env sigma0 ise c =
let match_upats_HO upats env sigma0 ise c =
let it_did_match = ref false in
+ let failed_because_of_TC = ref false in
let rec aux upats env sigma0 ise c =
let f, a = splay_app ise c in let i0 = ref (-1) in
let fpats = List.fold_right (filter_upat i0 f (Array.length a)) upats [] in
@@ -620,14 +621,18 @@ let match_upats_HO upats env sigma0 ise c =
raise (FoundUnif (ungen_upat lhs pt' u))
with FoundUnif _ as sigma_u -> raise sigma_u
| NoProgress -> it_did_match := true
- | _ -> () in
+ | Typeclasses_errors.TypeClassError
+ (_,Typeclasses_errors.UnsatisfiableConstraints _) ->
+ failed_because_of_TC:=true
+ | e when Errors.noncritical e -> () in
List.iter one_match fpats
done;
iter_constr_LR (aux upats env sigma0 ise) f;
Array.iter (aux upats env sigma0 ise) a
in
aux upats env sigma0 ise c;
- if !it_did_match then raise NoProgress
+ if !it_did_match then raise NoProgress;
+ !failed_because_of_TC
let prof_HO = mk_profiler "match_upats_HO";;
let match_upats_HO upats env sigma0 ise c =
@@ -697,13 +702,17 @@ let source () = match upats_origin, upats with
anomaly "mk_tpattern_matcher with no upats_origin" in
((fun env c h ~k ->
do_once upat_that_matched (fun () ->
+ let failed_because_of_TC = ref false in
try
match_upats_FO upats env sigma0 ise c;
- match_upats_HO upats env sigma0 ise c;
+ failed_because_of_TC:=match_upats_HO upats env sigma0 ise c;
raise NoMatch
with FoundUnif sigma_u -> sigma_u
| NoMatch when (not raise_NoMatch) ->
- errorstrm (source () ++ str "does not match any subterm of the goal")
+ if !failed_because_of_TC then
+ errorstrm (source ()++strbrk"matches but type classes inference fails")
+ else
+ errorstrm (source () ++ str "does not match any subterm of the goal")
| NoProgress when (not raise_NoMatch) ->
let dir = match upats_origin with Some (d,_) -> d | _ ->
anomaly "mk_tpattern_matcher with no upats_origin" in
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
index 4bea3b8..c40d965 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
@@ -3,17 +3,14 @@
(* This line is read by the Makefile's dist target: do not remove. *)
DECLARE PLUGIN "ssreflect"
-let ssrversion = "1.5";;
+let ssrversion = "1.6";;
let ssrAstVersion = 1;;
let () = Mltop.add_known_plugin (fun () ->
if Flags.is_verbose () && not !Flags.batch_mode then begin
Printf.printf "\nSmall Scale Reflection version %s loaded.\n" ssrversion;
Printf.printf "Copyright 2005-2014 Microsoft Corporation and INRIA.\n";
Printf.printf "Distributed under the terms of the CeCILL-B license.\n\n"
- end;
- (* Disable any semantics associated with bullets *)
- Goptions.set_string_option_value_gen
- (Some false) ["Bullet";"Behavior"] "None")
+ end)
"ssreflect"
;;
@@ -477,7 +474,7 @@ let _ =
Goptions.optdepr = false;
Goptions.optwrite = (fun b -> ssroldreworder := b) }
-let ssrhaveNOtcresolution = ref false
+let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false
let inHaveTCResolution = Libobject.declare_object {
(Libobject.default_object "SSRHAVETCRESOLUTION") with
@@ -1440,7 +1437,7 @@ let interp_modloc mr =
let ssrdisplaysearch gr env t =
let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in
- msg (hov 2 pr_res ++ fnl ())
+ msg_info (hov 2 pr_res ++ fnl ())
VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY
| [ "Search" ssr_search_arg(a) ssr_modlocs(mr) ] ->
@@ -3843,7 +3840,8 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
(mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n)))
in
pp(lazy(str"after: " ++ pr_constr oc));
- try applyn ~with_evars ~with_shelve:true ?beta n oc gl with _ -> raise dependent_apply_error
+ try applyn ~with_evars ~with_shelve:true ?beta n oc gl
+ with e when Errors.noncritical e -> raise dependent_apply_error
let pf_fresh_inductive_instance ind gl =
let sigma, env, it = project gl, pf_env gl, sig_it gl in
@@ -4133,7 +4131,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
let pat = List.find (fun t -> Intset.mem i (evars_of_term t)) patterns in
errorstrm(str"Pattern"++spc()++pr_constr_pat pat++spc()++
str"was not completely instantiated and one of its variables"++spc()++
- str"occurs in the type of another non instantieted pattern variable");
+ str"occurs in the type of another non-instantiated pattern variable");
end
in
(* the elim tactic, with the eliminator and the predicated we computed *)
@@ -4922,7 +4920,7 @@ let rwprocess_rule dir rule gl =
let t =
if red = 1 then Tacred.hnf_constr env sigma t0
else Reductionops.whd_betaiotazeta sigma t0 in
- pp(lazy(str"rewrule="++pr_constr t));
+ pp(lazy(str"rewrule="++pr_constr_pat t));
match kind_of_term t with
| Prod (_, xt, at) ->
let ise, x = Evarutil.new_evar env (create_evar_defs sigma) xt in
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
index f62e234..fc0b573 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
@@ -345,6 +345,7 @@ let unif_end env sigma0 ise0 pt ok =
let ise = Evarconv.consider_remaining_unif_problems 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
let ise2 = Typeclasses.resolve_typeclasses ~fail:true env ise1 in
if not (ok ise) then raise NoProgress else
if ise2 == ise1 then (s, uc, t)
@@ -569,6 +570,12 @@ exception FoundUnif of (evar_map * evar_universe_context * tpattern)
(* Note: we don't update env as we descend into the term, as the primitive *)
(* unification procedure always rejects subterms with bound variables. *)
+let dont_impact_evars_in cl =
+ let evs_in_cl = Evd.evars_of_term cl in
+ fun sigma -> Evar.Set.for_all (fun k ->
+ try let _ = Evd.find_undefined sigma k in true
+ with Not_found -> false) evs_in_cl
+
(* We are forced to duplicate code between the FO/HO matching because we *)
(* have to work around several kludges in unify.ml: *)
(* - w_unify drops into second-order unification when the pattern is an *)
@@ -577,7 +584,8 @@ exception FoundUnif of (evar_map * evar_universe_context * tpattern)
(* head is an evar or meta (e.g., it fails on ?1 = nat when ?1 : Type). *)
(* - w_unify expands let-in (zeta conversion) eagerly, whereas we want to *)
(* match a head let rigidly. *)
-let match_upats_FO upats env sigma0 ise =
+let match_upats_FO upats env sigma0 ise orig_c =
+ let dont_impact_evars = dont_impact_evars_in orig_c in
let rec loop c =
let f, a = splay_app ise c in let i0 = ref (-1) in
let fpats =
@@ -608,13 +616,13 @@ let match_upats_FO upats env sigma0 ise =
let lhs = mkSubApp f i a in
let pt' = unif_end env sigma0 ise' u.up_t (u.up_ok lhs) in
raise (FoundUnif (ungen_upat lhs pt' u))
- with FoundUnif _ as sigma_u -> raise sigma_u
+ with FoundUnif (s,_,_) as sig_u when dont_impact_evars s -> raise sig_u
| Not_found -> Errors.anomaly (str"incomplete ise in match_upats_FO")
| _ -> () in
List.iter one_match fpats
done;
iter_constr_LR loop f; Array.iter loop a in
- fun c -> try loop c with Invalid_argument _ -> Errors.anomaly (str"IN FO")
+ try loop orig_c with Invalid_argument _ -> Errors.anomaly (str"IN FO")
let prof_FO = mk_profiler "match_upats_FO";;
let match_upats_FO upats env sigma0 ise c =
@@ -623,7 +631,9 @@ let match_upats_FO upats env sigma0 ise c =
let match_upats_HO ~on_instance upats env sigma0 ise c =
+ let dont_impact_evars = dont_impact_evars_in c in
let it_did_match = ref false in
+ let failed_because_of_TC = ref false in
let rec aux upats env sigma0 ise c =
let f, a = splay_app ise c in let i0 = ref (-1) in
let fpats = List.fold_right (filter_upat i0 f (Array.length a)) upats [] in
@@ -652,16 +662,20 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
let lhs = mkSubApp f i a in
let pt' = unif_end env sigma0 ise'' u.up_t (u.up_ok lhs) in
on_instance (ungen_upat lhs pt' u)
- with FoundUnif _ as sigma_u -> raise sigma_u
+ with FoundUnif (s,_,_) as sig_u when dont_impact_evars s -> raise sig_u
| NoProgress -> it_did_match := true
- | _ -> () in
+ | Pretype_errors.PretypeError
+ (_,_,Pretype_errors.UnsatisfiableConstraints _) ->
+ failed_because_of_TC:=true
+ | e when Errors.noncritical e -> () in
List.iter one_match fpats
done;
iter_constr_LR (aux upats env sigma0 ise) f;
Array.iter (aux upats env sigma0 ise) a
in
aux upats env sigma0 ise c;
- if !it_did_match then raise NoProgress
+ if !it_did_match then raise NoProgress;
+ !failed_because_of_TC
let prof_HO = mk_profiler "match_upats_HO";;
let match_upats_HO ~on_instance upats env sigma0 ise c =
@@ -759,15 +773,19 @@ let rec uniquize = function
((fun env c h ~k ->
do_once upat_that_matched (fun () ->
+ let failed_because_of_TC = ref false in
try
if not all_instances then match_upats_FO upats env sigma0 ise c;
- match_upats_HO ~on_instance upats env sigma0 ise c;
+ failed_because_of_TC:=match_upats_HO ~on_instance upats env sigma0 ise c;
raise NoMatch
with FoundUnif sigma_u -> 0,[sigma_u]
| (NoMatch|NoProgress) when all_instances && instances () <> [] ->
0, uniquize (instances ())
| NoMatch when (not raise_NoMatch) ->
- errorstrm (source () ++ str "does not match any subterm of the goal")
+ if !failed_because_of_TC then
+ errorstrm (source ()++strbrk"matches but type classes inference fails")
+ else
+ errorstrm (source () ++ str "does not match any subterm of the goal")
| NoProgress when (not raise_NoMatch) ->
let dir = match upats_origin with Some (d,_) -> d | _ ->
Errors.anomaly (str"mk_tpattern_matcher with no upats_origin") in
@@ -1267,12 +1285,24 @@ let ssrpatterntac ist arg gl =
let (t, uc), concl_x =
fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in
let gl, tty = pf_type_of gl t in
- let concl = mkLetIn (Name (id_of_string "toto"), t, tty, concl_x) in
+ let concl = mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in
Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl
-TACTIC EXTEND ssrat
-| [ "ssrpattern" ssrpatternarg(arg) ] -> [ Proofview.V82.tactic (ssrpatterntac ist arg) ]
-END
+(* Register "ssrpattern" tactic *)
+let () =
+ let mltac _ ist =
+ let arg =
+ Genarg.out_gen (topwit wit_ssrpatternarg)
+ (Id.Map.find (Names.Id.of_string "ssrpatternarg") ist.lfun) in
+ Proofview.V82.tactic (ssrpatterntac ist arg) in
+ let name = { mltac_plugin = "ssreflect"; mltac_tactic = "ssrpattern"; } in
+ let () = Tacenv.register_ml_tactic name mltac in
+ let tac =
+ TacFun ([Some (Id.of_string "ssrpatternarg")],
+ TacML (Loc.ghost, name, [])) in
+ let obj () =
+ Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in
+ Mltop.declare_cache_obj obj "ssreflect"
let ssrinstancesof ist arg gl =
let ok rhs lhs ise = true in
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index b346a93..6b9720b 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -590,12 +590,6 @@ Proof. by move=> p_pr; rewrite /pdiv primes_exp ?primes_prime. Qed.
(* Primes are unbounded. *)
-Lemma dvdn_fact m n : 0 < m <= n -> m %| n`!.
-Proof.
-case: m => //= m; elim: n => //= n IHn; rewrite ltnS leq_eqVlt.
-by case/predU1P=> [-> | /IHn]; [apply: dvdn_mulr | apply: dvdn_mull].
-Qed.
-
Lemma prime_above m : {p | m < p & prime p}.
Proof.
have /pdivP[p pr_p p_dv_m1]: 1 < m`! + 1 by rewrite addn1 ltnS fact_gt0.
diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v
index 4a3cfc7..1ff82ab 100644
--- a/mathcomp/ssreflect/ssreflect.v
+++ b/mathcomp/ssreflect/ssreflect.v
@@ -51,6 +51,7 @@ Global Set Asymmetric Patterns.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
+Global Set Bullet Behavior "None".
Module SsrSyntax.
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 5091411..9b9f6a5 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -1121,8 +1121,8 @@ Proof.
by move=> le_nm; apply: (@canRL bool) (addbK _) _; rewrite -odd_add subnK.
Qed.
-Lemma odd_opp i m : odd m = false -> i < m -> odd (m - i) = odd i.
-Proof. by move=> oddm lt_im; rewrite (odd_sub (ltnW lt_im)) oddm. Qed.
+Lemma odd_opp i m : odd m = false -> i <= m -> odd (m - i) = odd i.
+Proof. by move=> oddm le_im; rewrite (odd_sub (le_im)) oddm. Qed.
Lemma odd_mul m n : odd (m * n) = odd m && odd n.
Proof. by elim: m => //= m IHm; rewrite odd_add -addTb andb_addl -IHm. Qed.
diff --git a/mathcomp/ssrtest/Make b/mathcomp/ssrtest/Make
index ab4c666..716dc4a 100644
--- a/mathcomp/ssrtest/Make
+++ b/mathcomp/ssrtest/Make
@@ -39,6 +39,7 @@ view_case.v
wlogletin.v
wlog_suff.v
wlong_intro.v
+tacnotationpattern.v
-R ../theories Ssreflect
-I ../src/
diff --git a/mathcomp/ssrtest/tacnotationpattern.v b/mathcomp/ssrtest/tacnotationpattern.v
new file mode 100644
index 0000000..13de4bc
--- /dev/null
+++ b/mathcomp/ssrtest/tacnotationpattern.v
@@ -0,0 +1,14 @@
+Require Import mathcomp.ssreflect.ssreflect.
+Tactic Notation "at" ssrpatternarg(p) tactic(t)
+ :=
+ ssrpattern p; let top := fresh in intro top;
+ t top; try unfold top in * |- *; try clear top.
+
+Goal forall x y, x + y = 4.
+intros.
+at [RHS] (fun top => remember top as E eqn:E_def).
+match goal with
+| |- x + y = E => idtac
+| |- _ => fail
+end.
+Admitted.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 03:46:32 +0000