aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-12-16 16:37:24 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-12-16 16:37:24 +0000
commit8b02832139cc699d6b5b557ef5badfc800c2589a (patch)
tree46a5c3ff220f996bdb50a252b40f9d2e14be1aa6 /proofs
parentcb6a9e95382bd90fb10a93e19c0189f546a476ea (diff)
Redondant or incompatible instantiations in clenv_assign now correctly trapped
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1136 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml15
1 files changed, 13 insertions, 2 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 66b3bddb2..1fe882caf 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -388,7 +388,18 @@ let clenv_assign mv rhs clenv =
error "clenv__assign: circularity in unification";
try
(match Intmap.find mv clenv.env with
- | Clval _ -> anomaly "clenv_assign: metavar already assigned"
+ | Clval (fls,ty) ->
+ if not (eq_constr fls.rebus rhs) then
+ try
+ (* Streams are lazy, force evaluation of id to catch Not_found*)
+ let id = Intmap.find mv clenv.namenv in
+ errorlabstrm "clenv_assign"
+ [< 'sTR "An incompatible instantiation has already been found for ";
+ pr_id id >]
+ with Not_found ->
+ anomaly "clenv_assign: non dependent metavar already assigned"
+ else
+ clenv
| Cltyp bty ->
{ templval = clenv.templval;
templtyp = clenv.templtyp;
@@ -873,7 +884,7 @@ let clenv_match_args s clause =
errorlabstrm "clenv_match_args"
[< 'sTR "The variable "; pr_id s;
'sTR " occurs more than once in binding" >]
- else
+ else
clenv_lookup_name clause s
| NoDep n ->
if List.mem_assoc b t then errorlabstrm "clenv_match_args"