diff options
| author | herbelin | 2000-06-03 16:37:37 +0000 |
|---|---|---|
| committer | herbelin | 2000-06-03 16:37:37 +0000 |
| commit | b4edfe015c54cb67fe1f5a029165e390539d960c (patch) | |
| tree | 9d8b1d0b481440603e81937eb9622cb124ce1472 /kernel/term.mli | |
| parent | 94b27cf1c88ba0473b4b59a81be93b1d7d1f9316 (diff) | |
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
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 18 |
1 files changed, 16 insertions, 2 deletions
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. *) |