diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-17 20:28:19 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-17 20:28:19 +0000 |
| commit | ed29c6bbe9a45e7d3996c230a6cc2bf7b11848f1 (patch) | |
| tree | f898c771227a1e111be1bac0431d42d04b0166f6 /pretyping/unification.mli | |
| parent | 59c2fa12e257ae6087e0580e0d7abca3552421b8 (diff) | |
restructuration des printers: proofs passe avant parsing
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 95b35a56c..fb2a7ebbd 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -9,18 +9,11 @@ (*i $Id$ i*) (*i*) -open Util -open Names open Term -open Sign open Environ open Evd -open Evarutil (*i*) -val w_Declare : env -> evar -> types -> evar_defs -> evar_defs -val w_Define : evar -> constr -> evar_defs -> evar_defs - (* The "unique" unification fonction *) val w_unify : bool -> env -> conv_pb -> constr -> constr -> evar_defs -> evar_defs @@ -35,6 +28,6 @@ val w_unify_to_subterm : (* [abstract_list_all env sigma t c l] *) (* abstracts the terms in l over c to get a term of type t *) -(* (used in inv.ml) *) +(* (exported for inv.ml) *) val abstract_list_all : env -> evar_map -> constr -> constr -> constr list -> constr |