diff options
| author | barras | 2002-04-10 15:49:50 +0000 |
|---|---|---|
| committer | barras | 2002-04-10 15:49:50 +0000 |
| commit | d69ce3d0733a7e306514734a2b56d7e112f84f1d (patch) | |
| tree | 8b2fe29ce72929fe8ec3cce5da59395107efd29a /proofs/clenv.mli | |
| parent | c5d7e4037655fb1c2e46961407ad371ed52e8995 (diff) | |
backtrack dans l'algo d'unification
fichier usage incorrect (libdir et bindir ont disparu)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2629 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/clenv.mli')
| -rw-r--r-- | proofs/clenv.mli | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 2514b6e754..e83d8d7d78 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -53,8 +53,6 @@ type 'a clausenv = { * [hook] is the pointer to the current walking context, for * integrating existential vars and metavars. *) -type wc = named_context sigma (* for a better reading of the following *) - val unify : constr -> tactic val unify_0 : Reductionops.conv_pb -> wc -> constr -> constr @@ -99,16 +97,9 @@ val clenv_type_of : wc clausenv -> constr -> constr val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv val make_clenv_binding_apply : - named_context sigma -> - int -> - constr * constr -> - (bindOcc * types) list -> - named_context sigma clausenv + wc -> int -> constr * types -> constr substitution -> wc clausenv val make_clenv_binding : - named_context sigma -> - constr * constr -> - (bindOcc * types) list -> - named_context sigma clausenv + wc -> constr * types -> constr substitution -> wc clausenv (* Exported for program.ml only *) val clenv_add_sign : |