diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-10 16:06:33 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 10:23:29 +0200 |
| commit | ce609ff2ae8bdf59d31919194a2e58d6feb43943 (patch) | |
| tree | 6a12557a042a49c6f127826e1b93aef9ae82c335 /pretyping/evd.ml | |
| parent | 2b12eb9574b7192d70605e9c707fc4b2f94b71d0 (diff) | |
Move the handling of the principal evar from refine to evd.
See previous commit for more discussion.
Changed the name from "main" to "principal" because I find "main" overused, and because the name was only introduced yesterday anyway.
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 25 |
1 files changed, 22 insertions, 3 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index c592ab9a5..35ca18e4f 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -585,8 +585,16 @@ type evar_map = { metas : clbinding Metamap.t; (** Interactive proofs *) effects : Declareops.side_effects; - future_goals : Evar.t list; (** list of newly created evars, - to be eventually turned into goals if not solved.*) + future_goals : Evar.t list; (** list of newly created evars, to be + eventually turned into goals if not solved.*) + principal_future_goal : Evar.t option; (** if [Some e], [e] must be + contained + [future_goals]. The evar + [e] will inherit + properties (now: the + name) of the evar which + will be instantiated with + a term containing [e]. *) } (*** Lifting primitive from Evar.Map. ***) @@ -796,6 +804,7 @@ let empty = { effects = Declareops.no_seff; evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *) future_goals = []; + principal_future_goal = None; } let from_env ?ctx e = @@ -984,10 +993,19 @@ let eval_side_effects evd = evd.effects let declare_future_goal evk evd = { evd with future_goals = evk::evd.future_goals } +let declare_principal_goal evk evd = + match evd.principal_future_goal with + | None -> { evd with + future_goals = evk::evd.future_goals; + principal_future_goal=Some evk; } + | Some _ -> Errors.error "Only one main subgoal per instantiation." + let future_goals evd = evd.future_goals +let principal_future_goal evd = evd.principal_future_goal + let reset_future_goals evd = - { evd with future_goals = [] } + { evd with future_goals = [] ; principal_future_goal=None } let meta_diff ext orig = Metamap.fold (fun m v acc -> @@ -1445,6 +1463,7 @@ let set_metas evd metas = { effects = evd.effects; evar_names = evd.evar_names; future_goals = evd.future_goals; + principal_future_goal = evd.principal_future_goal; } let meta_list evd = metamap_to_list evd.metas |