From 21bcc5f6fc8db1ccad16dea89f1705a799c1d090 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 27 Dec 2018 08:56:23 +0100
Subject: Notations: Enforce strong evaluation of cases_pattern_of_glob_constr.

This is because it can raise Not_found in depth and we need to catch
it at the right time.
---
 pretyping/glob_ops.ml  | 10 ++++++++--
 pretyping/glob_ops.mli |  1 +
 2 files changed, 9 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 6b61b1452e..68626597fc 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -485,7 +485,11 @@ let is_gvar id c = match DAst.get c with
 | GVar id' -> Id.equal id id'
 | _ -> false
 
-let rec cases_pattern_of_glob_constr na = DAst.map (function
+let rec cases_pattern_of_glob_constr na c =
+  (* Forcing evaluation to ensure that the possible raising of
+     Not_found is not delayed *)
+  let c = DAst.force c in
+  DAst.map (function
   | GVar id ->
     begin match na with
     | Name _ ->
@@ -498,6 +502,8 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function
   | GApp (c, l) ->
     begin match DAst.get c with
     | GRef (ConstructRef cstr,_) ->
+      let nparams = Inductiveops.inductive_nparams (fst cstr) in
+      let _,l = List.chop nparams l in
       PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
     | _ -> raise Not_found
     end
@@ -505,7 +511,7 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function
      (* A canonical encoding of aliases *)
      DAst.get (cases_pattern_of_glob_constr na' b)
   | _ -> raise Not_found
-  )
+  ) c
 
 open Declarations
 open Term
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 91a2ef9c1e..c189a3bcb2 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -89,6 +89,7 @@ val map_pattern : (glob_constr -> glob_constr) ->
 
 (** Conversion from glob_constr to cases pattern, if possible
 
+    Evaluation is forced.
     Take the current alias as parameter,
     @raise Not_found if translation is impossible *)
 val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g
-- 
cgit v1.2.3