diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-27 16:15:34 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-27 16:15:34 +0000 |
| commit | ecf68d1ed251e2c6b4abd9e97400d3ab009d2925 (patch) | |
| tree | 816959daf3aa5d5b7469ecc7c4bcc72e517aed76 /pretyping/unification.mli | |
| parent | e961ace331ec961dcec0e2525d7b9142d04b5154 (diff) | |
- Backtrack sur option with_types suite à confusion sur l'utilisation
des types des with-bindings dans la 8.1 [ceux-ci étaient déjà
utilisés et ce qui est vraiment nouveau est que l'unification est
maintenant celle de evarconv alors que c'était avant un mélange
d'unify_0 (sans delta) et de coercion sur les termes sans evars]. Je
renonce à maintenir la compatibilité (on se retrouve donc avec un
exemple qui fonctionne différement dans TermsConv.v de CoLoR).
- Robustesse accrue pour la nouvelle facilité de syntaxe de binding
avec paramètre pour pose/set.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10856 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 8cfa20948..1b8f9ccd8 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -17,12 +17,11 @@ open Evd type unify_flags = { modulo_conv_on_closed_terms : Names.transparent_state option; use_metas_eagerly : bool; - use_types : bool; modulo_delta : Names.transparent_state; } val default_unify_flags : unify_flags -val simple_apply_unify_flags : unify_flags +val default_no_delta_unify_flags : unify_flags (* The "unique" unification fonction *) val w_unify : |