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.ml | |
| 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.ml')
| -rw-r--r-- | proofs/clenv.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0c76be8df1..831267087d 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -82,8 +82,6 @@ type 'a clausenv = { env : clbinding Intmap.t; hook : 'a } -type wc = named_context sigma - let applyHead n c wc = let rec apprec n c cty wc = if n = 0 then @@ -133,7 +131,6 @@ let unify_r2l x = x let sort_eqns = unify_r2l - let unify_0 cv_pb wc m n = let env = w_env wc and sigma = w_Underlying wc in @@ -186,7 +183,8 @@ let unify_0 cv_pb wc m n = if (not(occur_meta m)) & is_fconv cv_pb env sigma m n then ([],[]) else - unirec_rec cv_pb ([],[]) m n + let (mc,ec) = unirec_rec cv_pb ([],[]) m n in + (sort_eqns mc, sort_eqns ec) (* Unification @@ -802,7 +800,7 @@ let clenv_unify allow_K cv_pb ty1 ty2 clenv = with ex when catchable_exception ex -> error "Cannot solve a second-order unification problem") - | _ -> clenv_typed_unify cv_pb ty1 ty2 clenv + | _ -> clenv_unify_0 cv_pb ty1 ty2 clenv (* [clenv_bchain mv clenv' clenv] |