diff options
| author | Cyril Cohen | 2017-12-14 19:09:33 +0100 |
|---|---|---|
| committer | GitHub | 2017-12-14 19:09:33 +0100 |
| commit | 7ed910eed93cbd5523a731998b1d2c87db712b94 (patch) | |
| tree | 2b4fee8639328862336311f8f30e006a6644c219 /mathcomp | |
| parent | e4e5648250de1354366aa3b0637f8d6d72f5180f (diff) | |
| parent | 7406d43614dda186492f8e8cc184783980aaa969 (diff) | |
Merge pull request #155 from erikmd/fix/gh-61
Update v8.5 plugin to fix math-comp/math-comp#61
Diffstat (limited to 'mathcomp')
5 files changed, 11 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/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 |