diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-03-15 16:51:10 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-03-15 16:51:10 +0000 |
| commit | 4a3a43565c54c3d987b57ecc4a8062777937222b (patch) | |
| tree | 34c43c6c0ca069f6c2e5a7008b2f846ac00f787d /pretyping/reductionops.mli | |
| parent | 5e034ee8d0e90e4b051de0e1aad889668b8e1ee2 (diff) | |
Backtrack sur la substitution combinée avec l'instanciation en réponse à l'inefficacité montrée dans le bug #932: suppression plutôt des Anonymous dans le contexte des evars (cf Evarutil)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6836 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index f8baac5ea..29a28f0f7 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -120,8 +120,6 @@ val hnf_lam_app : env -> evar_map -> constr -> constr -> constr val hnf_lam_appvect : env -> evar_map -> constr -> constr array -> constr val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr -val subst1_nf_evar : evar_map -> constr -> constr -> constr - val splay_prod : env -> evar_map -> constr -> (name * constr) list * constr val splay_lambda : env -> evar_map -> constr -> (name * constr) list * constr val splay_arity : env -> evar_map -> constr -> (name * constr) list * sorts |