diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/quote/quote.ml | 4 | ||||
| -rw-r--r-- | plugins/subtac/subtac_pretyping_F.ml | 22 | ||||
| -rw-r--r-- | plugins/subtac/subtac_utils.ml | 1 |
3 files changed, 14 insertions, 13 deletions
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 16cc3a7316..e1a16ce498 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -215,9 +215,9 @@ let compute_rhs bodyi index_of_f = let i = destRel (array_last args) in PMeta (Some (coerce_meta_in i)) | App (f,args) -> - PApp (pattern_of_constr f, Array.map aux args) + PApp (pattern_of_constr Evd.empty f, Array.map aux args) | Cast (c,_,_) -> aux c - | _ -> pattern_of_constr c + | _ -> pattern_of_constr Evd.empty c in aux bodyi diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index 7d1f2cd62e..f909f9e0a9 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -569,7 +569,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct error_unexpected_type_loc (loc_of_rawconstr c) env ( !evdref) tj.utj_val v - let pretype_gen fail_evar resolve_classes evdref env lvar kind c = + let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c = let c' = match kind with | OfType exptyp -> let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in @@ -581,7 +581,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct evdref := Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:fail_evar env !evdref; - let c = nf_evar !evdref c' in + let c = if expand_evar then nf_evar !evdref c' else c' in if fail_evar then check_evars env Evd.empty !evdref c; c @@ -606,30 +606,30 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct fail on unresolved evars; the unsafe_judgment list allows us to extend env with some bindings *) - let ise_pretype_gen fail_evar resolve_classes sigma env lvar kind c = + let ise_pretype_gen expand_evar fail_evar resolve_classes sigma env lvar kind c = let evdref = ref (Evd.create_evar_defs sigma) in - let c = pretype_gen fail_evar resolve_classes evdref env lvar kind c in + let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in !evdref, c (** Entry points of the high-level type synthesis algorithm *) let understand_gen kind sigma env c = - snd (ise_pretype_gen true true sigma env ([],[]) kind c) + snd (ise_pretype_gen true true true sigma env ([],[]) kind c) let understand sigma env ?expected_type:exptyp c = - snd (ise_pretype_gen true true sigma env ([],[]) (OfType exptyp) c) + snd (ise_pretype_gen true true true sigma env ([],[]) (OfType exptyp) c) let understand_type sigma env c = - snd (ise_pretype_gen false true sigma env ([],[]) IsType c) + snd (ise_pretype_gen true false true sigma env ([],[]) IsType c) - let understand_ltac sigma env lvar kind c = - ise_pretype_gen false true sigma env lvar kind c + let understand_ltac expand_evar sigma env lvar kind c = + ise_pretype_gen expand_evar false true sigma env lvar kind c let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c = - ise_pretype_gen false resolve_classes sigma env ([],[]) (OfType exptyp) c + ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c = - pretype_gen fail_evar resolve_classes evdref env ([],[]) kind c + pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c end module Default : S = SubtacPretyping_F(Coercion.Default) diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index 476724ba6d..32a1755ca0 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -189,6 +189,7 @@ let string_of_hole_kind = function | TomatchTypeParameter _ -> "TomatchTypeParameter" | GoalEvar -> "GoalEvar" | ImpossibleCase -> "ImpossibleCase" + | MatchingVar _ -> "MatchingVar" let evars_of_term evc init c = let rec evrec acc c = |