- Ajout de la possibilité d'utiliser la notation Record pour les

  coinductifs à un constructeur (suggestion de Georges). 
- Si pas de sorte ou arité mentionnée dans Inductive/CoInductive/Record,
  Type est utilisé comme défaut.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9917 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 13 insertions, 6 deletions

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 668b3a1eb4..d01c5679cc 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -989,14 +989,18 @@ let assums_of_rel_context sign =
         | None -> (na, t)::l)
     sign ~init:[]
 
-let lift_rel_context n sign =
-  let rec liftrec k = function
-    | (na,c,t)::sign ->
-	(na,option_map (liftn n k) c,type_app (liftn n k) t)
-	::(liftrec (k-1) sign)
+let map_rel_context_with_binders f sign =
+  let rec aux k = function
+    | d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign
     | [] -> []
   in
-  liftrec (rel_context_length sign) sign
+  aux (rel_context_length sign) sign
+
+let substl_rel_context l =
+  map_rel_context_with_binders (fun k -> substnl l (k-1))
+
+let lift_rel_context n =
+  map_rel_context_with_binders (liftn n)
 
 let fold_named_context_both_sides f l ~init = list_fold_right_and_left f l init
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 27e86a6ca5..17207cf577 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -218,6 +218,9 @@ val rename_bound_var : env -> identifier list -> types -> types
 val process_rel_context : (rel_declaration -> env -> env) -> env -> env
 val assums_of_rel_context : rel_context -> (name * constr) list
 val lift_rel_context : int -> rel_context -> rel_context
+val substl_rel_context : constr list -> rel_context -> rel_context
+val map_rel_context_with_binders : 
+  (int -> constr -> constr) -> rel_context -> rel_context
 val fold_named_context_both_sides :
   ('a -> named_declaration -> named_declaration list -> 'a) ->
     named_context -> init:'a -> 'a