diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/clenv.ml | 4 | ||||
| -rw-r--r-- | pretyping/clenv.mli | 4 | ||||
| -rw-r--r-- | pretyping/evd.ml | 4 | ||||
| -rw-r--r-- | pretyping/pattern.ml | 2 | ||||
| -rw-r--r-- | pretyping/typing.ml | 2 |
5 files changed, 9 insertions, 7 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 242368ce99..e5632515d0 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -261,8 +261,8 @@ let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl = * pose a value for it by constructing a fresh evar. We do this in * left-to-right order, so that every evar's type is always closed w.r.t. * metas. *) -let clenv_pose_dependent_evars clenv = - let dep_mvs = clenv_dependent false clenv in + +let clenv_pose_metas_as_evars clenv dep_mvs = List.fold_left (fun clenv mv -> let ty = clenv_meta_type clenv mv in diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 4f27ec902f..dfa7513495 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -79,7 +79,9 @@ val clenv_unique_resolver : val evar_clenv_unique_resolver : bool -> ?flags:unify_flags -> clausenv -> evar_info sigma -> clausenv -val clenv_pose_dependent_evars : clausenv -> clausenv +val clenv_dependent : bool -> clausenv -> metavariable list + +val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv (***************************************************************) (* Bindings *) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 2703e5ae0c..91b70e3b02 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -674,5 +674,5 @@ let pr_evar_defs evd = str"METAS:"++brk(0,1)++pr_meta_map evd.metas in v 0 (pp_evm ++ cstrs ++ pp_met) -let pr_metaset metas = - Metaset.fold (fun mv pp -> pr_meta mv ++ pp) metas (Pp.mt()) +let pr_metaset metas = + str "[" ++ prlist_with_sep spc pr_meta (Metaset.elements metas) ++ str "]" diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 90a3728ebb..05af1652e1 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -92,7 +92,7 @@ let head_of_constr_reference c = match kind_of_term c with let rec pattern_of_constr t = match kind_of_term t with | Rel n -> PRel n - | Meta n -> PMeta (Some (id_of_string (string_of_int n))) + | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n))) | Var id -> PVar id | Sort (Prop c) -> PSort (RProp c) | Sort (Type _) -> PSort (RType None) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 32df490db8..ece3586a19 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -23,7 +23,7 @@ open Evd let meta_type evd mv = let ty = try Evd.meta_ftype evd mv - with Not_found -> error ("unknown meta ?"^string_of_int mv) in + with Not_found -> anomaly ("unknown meta ?"^Nameops.string_of_meta mv) in meta_instance evd ty let constant_type_knowing_parameters env cst jl = |