diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-13 10:33:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-13 12:08:33 +0200 |
| commit | c06fa8b4c16c35fe48039d5b13e181cca9ebbb51 (patch) | |
| tree | a56051d2986315eb2da48c605bd3cd894796e041 /tactics/tactics.ml | |
| parent | c272523bb9d89fe55d1636b48728e7938a8230dd (diff) | |
Check resolution of Metas turned into Evars by pose_all_metas_as_evars
in unification.ml in case prefix 'e' of "apply" and co is not given.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 23c37fb65..984e165d1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -760,6 +760,18 @@ let error_uninstantiated_metas t clenv = let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta") in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".") +let check_unresolved_evars_of_metas clenv = + (* This checks that Metas turned into Evars by *) + (* Refiner.pose_all_metas_as_evars are resolved *) + List.iter (fun (mv,b) -> match b with + | Clval (_,(c,_),_) -> + (match kind_of_term c.rebus with + | Evar (evk,_) when Evd.is_undefined clenv.evd evk -> + error_uninstantiated_metas (mkMeta mv) clenv + | _ -> ()) + | _ -> ()) + (meta_list clenv.evd) + (* For a clenv expressing some lemma [C[?1:T1,...,?n:Tn] : P] and some goal [G], [clenv_refine_in] returns [n+1] subgoals, the [n] last ones (resp [n] first ones if [sidecond_first] is [true]) being the @@ -774,6 +786,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id c else clenv in let new_hyp_typ = clenv_type clenv in + if not with_evars then check_unresolved_evars_of_metas clenv; if not with_evars && occur_meta new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in |