summaryrefslogtreecommitdiff
path: root/pretyping/cases.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cases.ml')
-rw-r--r--pretyping/cases.ml29
1 files changed, 15 insertions, 14 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a4880f5e..c2d8921e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cases.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: cases.ml 12167 2009-06-06 20:07:22Z herbelin $ *)
open Util
open Names
@@ -130,7 +130,7 @@ let push_rel_defs =
(* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
-let regeneralize_rel i k j = if j = i+k then k else if j < i+k then j else j
+let regeneralize_rel i k j = if j = i+k then k+1 else j
let rec regeneralize_index i k t = match kind_of_term t with
| Rel j when j = i+k -> mkRel (k+1)
@@ -605,19 +605,13 @@ let find_dependencies_signature deps_in_rhs typs =
let _,l = List.fold_right2 find_dependencies deps_in_rhs typs (k,[]) in
List.map (fun (_,deps,_) -> deps) l
-(******)
+(* Assume we had terms t1..tq to match in a context xp:Tp,...,x1:T1 |-
+ and xn:Tn has just been regeneralized into x:Tn so that the terms
+ to match are now to be considered in the context xp:Tp,...,x1:T1,x:Tn |-.
-(* A Pushed term to match has just been substituted by some
- constructor t = (ci x1...xn) and the terms x1 ... xn have been added to
- match
-
- - all terms to match and to push (dependent on t by definition)
- must have (Rel depth) substituted by t and Rel's>depth lifted by n
- - all pushed terms to match (non dependent on t by definition) must
- be lifted by n
-
- We start with depth=1
-*)
+ [regeneralize_index_tomatch n tomatch] updates t1..tq so that
+ former references to xn are now references to x. Note that t1..tq
+ are already adjusted to the context xp:Tp,...,x1:T1,x:Tn |-. *)
let regeneralize_index_tomatch n =
let rec genrec depth = function
@@ -661,6 +655,13 @@ let replace_tomatch n c =
let liftn_rel_declaration n k = map_rel_declaration (liftn n k)
let substnl_rel_declaration sigma k = map_rel_declaration (substnl sigma k)
+(* [liftn_tomatch_stack]: a term to match has just been substituted by
+ some constructor t = (ci x1...xn) and the terms x1 ... xn have been
+ added to match; all pushed terms to match must be lifted by n
+ (knowing that [Abstract] introduces a binder in the list of pushed
+ terms to match).
+*)
+
let rec liftn_tomatch_stack n depth = function
| [] -> []
| Pushed ((c,tm),l,dep)::rest ->