diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-23 21:38:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-23 22:58:51 +0200 |
| commit | 5bddbf141cc6462563cdc86dcc7c02edccd295fd (patch) | |
| tree | 9ebc3de6396f376064b67c5da0202b1e33ed22af /proofs/goal.ml | |
| parent | 74ddca99c649f2f8c203582a9b82bddf64fb6b52 (diff) | |
Better representation of evar filters: we represent the vacuous filters of
any length with a [None] representation and ensure that this representation
is canonical through the restricted interface.
Diffstat (limited to 'proofs/goal.ml')
| -rw-r--r-- | proofs/goal.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 64eeb69d9..ac3e593da 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -501,8 +501,7 @@ module V82 = struct let mk_goal evars hyps concl extra = let evi = { Evd.evar_hyps = hyps; Evd.evar_concl = concl; - Evd.evar_filter = Evd.Filter.identity - (List.length (Environ.named_context_of_val hyps)); + Evd.evar_filter = Evd.Filter.identity; Evd.evar_body = Evd.Evar_empty; Evd.evar_source = (Loc.ghost,Evar_kinds.GoalEvar); Evd.evar_candidates = None; @@ -558,8 +557,8 @@ module V82 = struct let hyps = evi.Evd.evar_hyps in let new_hyps = List.fold_right Environ.push_named_context_val extra_hyps hyps in - let extra_filter = Evd.Filter.identity (List.length extra_hyps) in - let new_filter = Evd.Filter.append extra_filter evi.Evd.evar_filter in + let filter = evi.Evd.evar_filter in + let new_filter = Evd.Filter.extend (List.length extra_hyps) filter in let new_evi = { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in let new_evi = Typeclasses.mark_unresolvable new_evi in |