diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-25 11:42:32 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-25 11:42:32 +0000 |
| commit | 166714d89845f7e2f894fcd0fd92ae16961ca9eb (patch) | |
| tree | 031e532e4fbeb9520424b5246280d2e4994f2b01 /contrib | |
| parent | dd693ba7f6622ea14c11cbae4eb258e06a852b7e (diff) | |
- Fix bug in eterm which was not taking filtered contexts in evars into
account.
- Add test case for bug #1844 on Combined Scheme.
- Change Reflexive_partial_app_morphism to require a Reflexive proof to
cut down search earlier, without losing anything.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10846 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/subtac/eterm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 9cb65f76e..8f319f9ef 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -141,7 +141,7 @@ let eterm_obligations env name isevars evm fs t ty = (* Remove existential variables in types and build the corresponding products *) fold_right (fun (id, (n, nstr), ev) l -> - let hyps = Environ.named_context_of_val ev.evar_hyps in + let hyps = Evd.evar_filtered_context ev in let hyps = trunc_named_context nc_len hyps in let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in let evtyp, hyps, chop = |