From 9c3b440cfb2056d26acb30fbd0669d1635970246 Mon Sep 17 00:00:00 2001
From: pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 30 May 2013 12:52:30 +0000
Subject: Why not going inside fixpoint definition with appcontext ?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16544 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/matching.ml | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 1af1eae67..979a7dae3 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -351,8 +351,24 @@ let sub_match ?(partial_app=false) ?(closed=true) pat c =
       in
       let next = lazy (try_aux (c1 :: Array.to_list lc) next_mk_ctx next) in
       authorized_occ partial_app closed pat c mk_ctx next
-  | Construct _ | Fix _ | Ind _|CoFix _ |Evar _|Const _
-  | Rel _|Meta _|Var _|Sort _ ->
+  | Fix (indx,(names,types,bodies)) ->
+    let nb_fix = Array.length types in
+    let next_mk_ctx le =
+      let (ntypes,nbodies) = CList.chop nb_fix le in
+      mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in
+    let next = lazy
+      (try_aux
+	 ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next) in
+    authorized_occ partial_app closed pat c mk_ctx next
+  | CoFix (i,(names,types,bodies)) ->
+    let nb_fix = Array.length types in
+    let next_mk_ctx le =
+      let (ntypes,nbodies) = CList.chop nb_fix le in
+      mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in
+    let next = lazy
+      (try_aux ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next) in
+    authorized_occ partial_app closed pat c mk_ctx next
+  | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ ->
       authorized_occ partial_app closed pat c mk_ctx next
 
   (* Tries [sub_match] for all terms in the list *)
-- 
cgit v1.2.3