From b4edfe015c54cb67fe1f5a029165e390539d960c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 3 Jun 2000 16:37:37 +0000
Subject: Retrait des lam_and_pop and co; ajout d'un destructeur 'lispien' de
 constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@497 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.mli | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index 69bd7d644f..bfeccb0c72 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -428,7 +428,7 @@ val nb_lam : constr -> int
 (* similar to [nb_lam], but gives the number of products instead *)
 val nb_prod : constr -> int
 
-
+(* Trop compliqué
 (*s Various utility functions for implementing terms with bindings. *)
 
 val extract_lifted : int * constr -> constr
@@ -502,7 +502,7 @@ val lam_and_popl_named :
    properly lifted, and then push back the products, but as lambda-
    abstractions *)
 val lambda_ize : int ->'a oper term -> 'a oper term -> 'a oper term
-
+*)
 
 (*s Flattening and unflattening of embedded applications and casts. *)
 
@@ -573,6 +573,20 @@ val subst_term_occ : int list -> constr -> constr -> constr
 
 val subst_meta : (int * constr) list -> constr -> constr
 
+type constr_operator =
+  | OpMeta of int
+  | OpSort of sorts
+  | OpRel of int | OpVar of identifier
+  | OpCast | OpProd of name | OpLambda of name
+  | OpAppL | OpConst of section_path | OpAbst of section_path
+  | OpEvar of existential_key
+  | OpMutInd of inductive_path
+  | OpMutConstruct of constructor_path
+  | OpMutCase of case_info
+  | OpRec of fix_kind
+
+val splay_constr : constr -> constr_operator * constr list
+val gather_constr : constr_operator * constr list -> constr
 
 (*s Hash-consing functions for constr. *)
 
-- 
cgit v1.2.3