diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-27 10:25:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-27 10:25:19 +0000 |
| commit | 7b0c76beedf0e4e59c03701ee776a7c1dae58e20 (patch) | |
| tree | a58bb53276a0b2e9bbb7cb960e10f3e1563a2f1a /proofs | |
| parent | 662b0706737224e981f912a49614d33927699231 (diff) | |
Branchement du mécanisme d'instantiation des Evar en présence de définitions locales vers Evarutil
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@970 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 1332e0ecd..5ce77f413 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -32,9 +32,8 @@ type 'a clausenv = { type wc = walking_constraints let new_evar_in_sign env = - let ids = ids_of_named_context (Environ.named_context env) in let ev = new_evar () in - mkEvar (ev, Array.of_list (List.map mkVar ids)) + mkEvar (ev, Array.of_list (Evarutil.make_evar_instance env)) let rec whd_evar sigma t = match kind_of_term t with | IsEvar (ev,_ as evc) when is_defined sigma ev -> @@ -127,17 +126,19 @@ let unify_0 mc wc m n = | _, IsEvar _ -> metasubst,((cN,cM)::evarsubst) - | IsConst _, _ -> + | (IsConst _ | IsVar _ | IsRel _), _ -> if is_conv env sigma cM cN then substn else error_cannot_unify CCI (m,n) - | _, IsConst _ -> + | _, (IsConst _ | IsVar _| IsRel _) -> if (not (occur_meta cM)) & is_conv env sigma cM cN then substn else error_cannot_unify CCI (m,n) + + | IsLetIn (_,b,_,c), _ -> unirec_rec substn (subst1 b c) cN | _ -> error_cannot_unify CCI (m,n) |