aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-27 10:25:19 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-27 10:25:19 +0000
commit7b0c76beedf0e4e59c03701ee776a7c1dae58e20 (patch)
treea58bb53276a0b2e9bbb7cb960e10f3e1563a2f1a /proofs
parent662b0706737224e981f912a49614d33927699231 (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.ml9
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)