From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 pretyping/patternops.ml | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

(limited to 'pretyping/patternops.ml')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index af46c390..fe73b610 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Globnames
@@ -123,6 +123,7 @@ let head_of_constr_reference c = match kind_of_term c with
 
 let pattern_of_constr env sigma t =
   let rec pattern_of_constr env t =
+  let open Context.Rel.Declaration in
   match kind_of_term t with
     | Rel n  -> PRel n
     | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n)))
@@ -132,11 +133,11 @@ let pattern_of_constr env sigma t =
     | Sort (Type _) -> PSort (GType [])
     | Cast (c,_,_)      -> pattern_of_constr env c
     | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,
-				  pattern_of_constr (push_rel (na,Some c,t) env) b)
+				  pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b)
     | Prod (na,c,b)   -> PProd (na,pattern_of_constr env c,
-				pattern_of_constr (push_rel (na, None, c) env) b)
+				pattern_of_constr (push_rel (LocalAssum (na, c)) env) b)
     | Lambda (na,c,b) -> PLambda (na,pattern_of_constr env c,
-				  pattern_of_constr (push_rel (na, None, c) env) b)
+				  pattern_of_constr (push_rel (LocalAssum (na, c)) env) b)
     | App (f,a) ->
         (match
           match kind_of_term f with
@@ -316,6 +317,10 @@ let rev_it_mkPLambda = List.fold_right mkPLambda
 
 let err loc pp = user_err_loc (loc,"pattern_of_glob_constr", pp)
 
+let warn_cast_in_pattern =
+  CWarnings.create ~name:"cast-in-pattern" ~category:"automation"
+    (fun () -> Pp.strbrk "Casts are ignored in patterns")
+
 let rec pat_of_raw metas vars = function
   | GVar (_,id) ->
       (try PRel (List.index Name.equal (Name id) vars)
@@ -347,7 +352,7 @@ let rec pat_of_raw metas vars = function
   | GHole _ ->
       PMeta None
   | GCast (_,c,_) ->
-      Pp.msg_warning (strbrk "Cast not taken into account in constr pattern");
+      warn_cast_in_pattern ();
       pat_of_raw metas vars c
   | GIf (_,c,(_,None),b1,b2) ->
       PIf (pat_of_raw metas vars c,
-- 
cgit v1.2.3