diff options
| -rw-r--r-- | mathcomp/ssreflect/Makefile.coq-makefile | 5 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 9 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssreflect_plugin.mllib | 1 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 | 8 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssrmatching.v | 7 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssrmatching_plugin.mllib | 1 |
6 files changed, 20 insertions, 11 deletions
diff --git a/mathcomp/ssreflect/Makefile.coq-makefile b/mathcomp/ssreflect/Makefile.coq-makefile index 68bfbc2..bf8115e 100644 --- a/mathcomp/ssreflect/Makefile.coq-makefile +++ b/mathcomp/ssreflect/Makefile.coq-makefile @@ -4,7 +4,8 @@ define coqmakefile MLLIB=;\ EXTRA=;\ case $(V) in\ - v8.5*|v8.4*)\ + v8.5*|v8.4*)\ + $$LN $(1)/plugin/$(V)/ssrmatching_plugin.mllib .;\ $$LN $(1)/plugin/$(V)/ssrmatching.mli .;\ $$LN $(1)/plugin/$(V)/ssrmatching.ml4 .;\ $$LN $(1)/plugin/$(V)/ssrmatching.v .;\ @@ -13,7 +14,7 @@ define coqmakefile $$LN $(1)/plugin/$(V)/ssrbool.v $(1)/;\ $$LN $(1)/plugin/$(V)/ssrfun.v $(1)/;\ $$LN $(1)/plugin/$(V)/ssreflect.v $(1)/;\ - MLLIB=ssreflect_plugin.mllib;\ + MLLIB="ssrmatching_plugin.mllib ssreflect_plugin.mllib";\ EXTRA="ssrmatching.mli ssrmatching.ml4 ssrmatching.v ssreflect.ml4";\ ;;\ v8.6*)\ diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index a517c8a..67454ac 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1159,6 +1159,14 @@ rewrite !(big_mkcond _ P) unlock. by elim: r1 => /= [|i r1 ->]; rewrite (mul1m, mulmA). Qed. +Lemma big_allpairs I1 I2 (r1 : seq I1) (r2 : seq I2) F : + \big[*%M/1]_(i <- [seq (i1, i2) | i1 <- r1, i2 <- r2]) F i = + \big[*%M/1]_(i1 <- r1) \big[op/idx]_(i2 <- r2) F (i1, i2). +Proof. +elim: r1 => [|i1 r1 IHr1]; first by rewrite !big_nil. +by rewrite big_cat IHr1 big_cons big_map. +Qed. + Lemma big_pred1_eq (I : finType) (i : I) F : \big[*%M/1]_(j | j == i) F j = F i. Proof. by rewrite -big_filter filter_index_enum enum1 big_seq1. Qed. @@ -1504,6 +1512,7 @@ Implicit Arguments reindex [R op idx I J P F]. Implicit Arguments reindex_inj [R op idx I h P F]. Implicit Arguments pair_big_dep [R op idx I J]. Implicit Arguments pair_big [R op idx I J]. +Implicit Arguments big_allpairs [R op idx I1 I2 r1 r2 F]. Implicit Arguments exchange_big_dep [R op idx I J rI rJ P Q F]. Implicit Arguments exchange_big_dep_nat [R op idx m1 n1 m2 n2 P Q F]. Implicit Arguments big_ord_recl [R op idx]. diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect_plugin.mllib b/mathcomp/ssreflect/plugin/v8.5/ssreflect_plugin.mllib index 006b70f..dee851c 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssreflect_plugin.mllib +++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect_plugin.mllib @@ -1,2 +1 @@ -Ssrmatching Ssreflect diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 index 658966b..ebc4de9 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 +++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 @@ -49,11 +49,11 @@ open Notation_ops open Locus open Locusops -DECLARE PLUGIN "ssreflect" +DECLARE PLUGIN "ssrmatching_plugin" type loc = Loc.t let dummy_loc = Loc.ghost -let errorstrm = Errors.errorlabstrm "ssreflect" +let errorstrm = Errors.errorlabstrm "ssrmatching" let loc_error loc msg = Errors.user_err_loc (loc, msg, str msg) (* 0 cost pp function. Active only if env variable SSRDEBUG is set *) @@ -1334,14 +1334,14 @@ let () = 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 name = { mltac_plugin = "ssrmatching_plugin"; 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" + Mltop.declare_cache_obj obj "ssrmatching_plugin" let ssrinstancesof ist arg gl = let ok rhs lhs ise = true in diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.v b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.v index 369ffaf..c20c846 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.v +++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.v @@ -1,9 +1,6 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. +Declare ML Module "ssrmatching_plugin". Module SsrMatchingSyntax. @@ -25,3 +22,5 @@ Notation LHS := (X in X = _)%pattern. End SsrMatchingSyntax. Export SsrMatchingSyntax. + +Tactic Notation "ssrpattern" ssrpatternarg(p) := ssrpattern p . diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching_plugin.mllib b/mathcomp/ssreflect/plugin/v8.5/ssrmatching_plugin.mllib new file mode 100644 index 0000000..5fb1f15 --- /dev/null +++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching_plugin.mllib @@ -0,0 +1 @@ +Ssrmatching |