Merge remote-tracking branch 'upstream/master' into fixdoc

5 files changed, 75 insertions, 14 deletions

diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
index c40d965..1c16fa9 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
@@ -1,17 +1,17 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 
 (* This line is read by the Makefile's dist target: do not remove. *)
-DECLARE PLUGIN "ssreflect"
+DECLARE PLUGIN "ssreflect_plugin"
 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 "Copyright 2005-2016 Microsoft Corporation and INRIA.\n";
     Printf.printf "Distributed under the terms of the CeCILL-B license.\n\n"
   end)
-  "ssreflect"
+  "ssreflect_plugin"
 ;;
 
 (* Defining grammar rules with "xx" in it automatically declares keywords too,
@@ -1011,7 +1011,7 @@ let pf_unabs_evars gl ise n c0 =
 type ssrargfmt = ArgSsr of string | ArgCoq of argument_type | ArgSep of string
 
 let ssrtac_name name = {
-  mltac_plugin = "ssreflect";
+  mltac_plugin = "ssreflect_plugin";
   mltac_tactic = "ssr" ^ name;
 }
 
@@ -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.5/ssreflect.mllib b/mathcomp/ssreflect/plugin/v8.5/ssreflect_plugin.mllib
index 006b70f..006b70f 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.mllib
+++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect_plugin.mllib
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
index fc0b573..084aee9 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 
 (* Defining grammar rules with "xx" in it automatically declares keywords too,
@@ -878,7 +878,36 @@ let pr_ssrpattern_roundp  _ _ _ = pr_pattern_roundp
 
 let wit_rpatternty = add_genarg "rpatternty" pr_pattern
 
-ARGUMENT EXTEND rpattern TYPED AS rpatternty PRINTED BY pr_rpattern
+let glob_ssrterm gs = function
+  | k, (_, Some c) -> k,
+      let x = Tacintern.intern_constr gs c in
+      fst x, Some c
+  | ct -> ct
+
+let glob_rpattern s p =
+  match p with
+  | T t -> T (glob_ssrterm 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)
+  | E_In_X_In_T(e,x,t) -> E_In_X_In_T (glob_ssrterm s e,x,glob_ssrterm s t)
+  | E_As_X_In_T(e,x,t) -> E_As_X_In_T (glob_ssrterm s e,x,glob_ssrterm s t)
+
+let subst_ssrterm s (k, c) = k, Tacsubst.subst_glob_constr_and_expr s c
+
+let subst_rpattern s = function
+  | T t -> T (subst_ssrterm s t)
+  | In_T t -> In_T (subst_ssrterm s t)
+  | X_In_T(x,t) -> X_In_T (x,subst_ssrterm s t)
+  | In_X_In_T(x,t) -> In_X_In_T (x,subst_ssrterm s t)
+  | E_In_X_In_T(e,x,t) -> E_In_X_In_T (subst_ssrterm s e,x,subst_ssrterm s t)
+  | E_As_X_In_T(e,x,t) -> E_As_X_In_T (subst_ssrterm s e,x,subst_ssrterm s t)
+
+ARGUMENT EXTEND rpattern
+  TYPED AS rpatternty
+  PRINTED BY pr_rpattern
+  GLOBALIZED BY glob_rpattern
+  SUBSTITUTED BY subst_rpattern
   | [ lconstr(c) ] -> [ T (mk_lterm c) ]
   | [ "in" lconstr(c) ] -> [ In_T (mk_lterm c) ]
   | [ lconstr(x) "in" lconstr(c) ] -> 
@@ -1264,12 +1293,17 @@ let is_wildcard = function
   | _ -> false
 
 (* "ssrpattern" *)
-let pr_ssrpatternarg _ _ _ cpat = pr_rpattern cpat
+let pr_ssrpatternarg _ _ _ (_,cpat) = pr_rpattern cpat
+let pr_ssrpatternarg_glob _ _ _ cpat = pr_rpattern cpat
+let interp_ssrpatternarg ist gl p = project gl, (ist, p)
 
 ARGUMENT EXTEND ssrpatternarg
-  TYPED AS rpattern
   PRINTED BY pr_ssrpatternarg
-| [ "[" rpattern(pat) "]" ] -> [ pat ]
+  INTERPRETED BY interp_ssrpatternarg
+  GLOBALIZED BY glob_rpattern
+  RAW_TYPED AS rpattern RAW_PRINTED BY pr_ssrpatternarg_glob
+  GLOB_TYPED AS rpattern GLOB_PRINTED BY pr_ssrpatternarg_glob
+| [ rpattern(pat) ] -> [ pat ]
 END
   
 let pf_merge_uc uc gl =
@@ -1278,8 +1312,8 @@ let pf_merge_uc uc gl =
 let pf_unsafe_merge_uc uc gl =
   re_sig (sig_it gl) (Evd.set_universe_context (project gl) uc)
 
-let ssrpatterntac ist arg gl =
-  let pat = interp_rpattern ist gl arg in
+let ssrpatterntac _ist (arg_ist,arg) gl =
+  let pat = interp_rpattern arg_ist gl arg in
   let sigma0 = project gl in
   let concl0 = pf_concl gl in
   let (t, uc), concl_x =
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli
index 74a603e..84700d6 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli
@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 
 open Genarg
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.v b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.v
new file mode 100644
index 0000000..369ffaf
--- /dev/null
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.v
@@ -0,0 +1,27 @@
+(* (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.
+
+Module SsrMatchingSyntax.
+
+(* Reserve the notation for rewrite patterns so that the user is not allowed  *)
+(* to declare it at a different level.                                        *)
+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).
+
+(* Notation to define shortcuts for the "X in t" part of a pattern.           *)
+Notation "( X 'in' t )" := (_ : fun X => t) : ssrpatternscope.
+Delimit Scope ssrpatternscope with pattern.
+
+(* Some shortcuts for recurrent "X in t" parts.                               *)
+Notation RHS := (X in _ = X)%pattern.
+Notation LHS := (X in X = _)%pattern.
+
+End SsrMatchingSyntax.
+
+Export SsrMatchingSyntax.