diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-03-10 14:48:31 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-03-10 14:48:31 +0000 |
| commit | d9f98fee95838b9d9cf83d218a0d927c04a38870 (patch) | |
| tree | 4ac6a22a9a8652148a1e8b9d04ab04c7ecd20c5e /pretyping/evarconv.ml | |
| parent | a2d79ff2330aa931b8cec08b92d8a9ee72c6c53b (diff) | |
Reparation bug isevars dans pretyping
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@309 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d80810af5..539a953a1 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -324,7 +324,7 @@ and conv_record env isevars (c,bs,(xs,xs1),(us,us1),(ts,ts1),t) = let ks = List.fold_left (fun ks b -> - let (k,_) = new_isevar isevars env (substl ks b) CCI in (k::ks)) + (new_isevar isevars env (substl ks b) CCI)::ks) [] bs in if (list_for_all2eq |