From 9e8c57419b473fdb3f9fbb8251d1843ec0e6f884 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 4 Oct 2016 13:27:29 +0200
Subject: Quick fix to #4595 (making notations containing "ltac:" unused for
 printing).

Also getting rid of a global side-effect.
---
 interp/constrintern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f98873aa66..194f5f1c2b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2013,14 +2013,14 @@ let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
 						tmp_scope = None; scopes = []; impls = impls}
     false (empty_ltac_sign, vl) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
-  let a = notation_constr_of_glob_constr nenv c in
+  let a, reversible = notation_constr_of_glob_constr nenv c in
   (* Splits variables into those that are binding, bound, or both *)
   (* binding and bound *)
   let out_scope = function None -> None,[] | Some (a,l) -> a,l in
   let vars = Id.Map.map (fun (isonlybinding, sc, typ) ->
     (!isonlybinding, out_scope !sc, typ)) vl in
   (* Returns [a] and the ordered list of variables with their scopes *)
-  vars, a
+  vars, a, reversible
 
 (* Interpret binders and contexts  *)
 
-- 
cgit v1.2.3


From 1969e10f25df0c913600099b7b98ea273a064017 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 4 Oct 2016 19:38:40 +0200
Subject: Fix #5048 - Casts in pattern raise an anomaly in Constrintern.

We protect the code against the presence of pattern casts where they are
not supported. Why we cannot make the pattern type reflect this is
a long story (described in this commit), but in the long term we
probably want to support them anywhere, like OCaml does. Of course, it
will require to adjust the pattern matching compiler.
---
 interp/constrintern.ml | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 194f5f1c2b..e6340646f5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1410,7 +1410,40 @@ let rec intern_pat genv aliases pat =
       check_or_pat_variables loc ids (List.tl idsl);
       (ids,List.flatten pl')
 
+(* [check_no_patcast p] raises an error if [p] contains a cast. This code is a
+   bit ad-hoc, and is due to current restrictions on casts in patterns. We
+   support them only in local binders and only at top level. In fact, they are
+   currently eliminated by the parser. The only reason why they are in the
+   [cases_pattern_expr] type is that the parser needs to factor the "(c : t)"
+   notation with user defined notations (such as the pair). In the long term, we
+   will try to support such casts everywhere, and use them to print the domains
+   of lambdas in the encoding of match in constr. We put this check here and not
+   in the parser because it would require to duplicate the levels of the
+   [pattern] rule. *)
+let rec check_no_patcast = function
+  | CPatCast (loc,_,_) ->
+     CErrors.user_err_loc (loc, "check_no_patcast",
+                           Pp.strbrk "Casts are not supported here.")
+  | CPatDelimiters(_,_,p)
+  | CPatAlias(_,p,_) -> check_no_patcast p
+  | CPatCstr(_,_,opl,pl) ->
+     Option.iter (List.iter check_no_patcast) opl;
+     List.iter check_no_patcast pl
+  | CPatOr(_,pl) ->
+     List.iter check_no_patcast pl
+  | CPatNotation(_,_,subst,pl) ->
+     check_no_patcast_subst subst;
+     List.iter check_no_patcast pl
+  | CPatRecord(_,prl) ->
+     List.iter (fun (_,p) -> check_no_patcast p) prl
+  | CPatAtom _ | CPatPrim _ -> ()
+
+and check_no_patcast_subst (pl,pll) =
+  List.iter check_no_patcast pl;
+  List.iter (List.iter check_no_patcast) pll
+
 let intern_cases_pattern genv scopes aliases pat =
+  check_no_patcast pat;
   intern_pat genv aliases
     (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat)
 
@@ -1419,6 +1452,7 @@ let _ =
     fun scopes p -> intern_cases_pattern (Global.env ()) scopes empty_alias p
 
 let intern_ind_pattern genv scopes pat =
+  check_no_patcast pat;
   let no_not =
     try
       drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat
-- 
cgit v1.2.3