diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/clenv.ml | 7 | ||||
| -rw-r--r-- | pretyping/clenv.mli | 4 | ||||
| -rw-r--r-- | pretyping/evd.ml | 3 | ||||
| -rw-r--r-- | pretyping/evd.mli | 1 | ||||
| -rw-r--r-- | pretyping/termops.ml | 4 | ||||
| -rw-r--r-- | pretyping/unification.ml | 13 | ||||
| -rw-r--r-- | pretyping/unification.mli | 4 |
7 files changed, 20 insertions, 16 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 2533e64e4..793ac2c32 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -218,7 +218,8 @@ let clenv_wtactic f clenv = {clenv with evd = f clenv.evd } * returns a list of the metavars which appear in the type of * the metavar mv. The list is unordered. *) -let clenv_metavars clenv mv = (meta_ftype clenv mv).freemetas +let clenv_metavars evd mv = + (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas let dependent_metas clenv mvs conclmetas = List.fold_right @@ -269,9 +270,7 @@ let clenv_pose_dependent_evars clenv = clenv dep_mvs -let evar_clenv_unique_resolver clenv gls = - clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls) - +let evar_clenv_unique_resolver = clenv_unique_resolver (******************************************************************) diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index ccaa22f5e..73a171b8d 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -75,9 +75,9 @@ val clenv_unique_resolver : bool -> clausenv -> evar_info sigma -> clausenv (* same as above ([allow_K=false]) but replaces remaining metas - with fresh evars *) + with fresh evars if [evars_flag] is [true] *) val evar_clenv_unique_resolver : - clausenv -> evar_info sigma -> clausenv + bool -> clausenv -> evar_info sigma -> clausenv val clenv_pose_dependent_evars : clausenv -> clausenv diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 300b4c8e6..d0cbeb574 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -659,3 +659,6 @@ let pr_evar_defs evd = if evd.metas = Metamap.empty then mt() else 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()) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index b5a36c1f3..5d03fbfd3 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -215,3 +215,4 @@ val pr_evar_info : evar_info -> Pp.std_ppcmds val pr_evar_map : evar_map -> Pp.std_ppcmds val pr_evar_defs : evar_defs -> Pp.std_ppcmds val pr_sort_constraints : evar_map -> Pp.std_ppcmds +val pr_metaset : Metaset.t -> Pp.std_ppcmds diff --git a/pretyping/termops.ml b/pretyping/termops.ml index f15ec5166..e52d7c82a 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -517,8 +517,8 @@ let free_rels m = let collect_metas c = let rec collrec acc c = match kind_of_term c with - | Meta mv -> mv::acc - | _ -> fold_constr collrec acc c + | Meta mv -> list_add_set mv acc + | _ -> fold_constr collrec acc c in List.rev (collrec [] c) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 52093e5af..b2190c53c 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -32,18 +32,20 @@ let abstract_scheme env c l lname_typ = List.fold_left2 (fun t (locc,a) (na,_,ta) -> let na = match kind_of_term a with Var id -> Name id | _ -> na in +(* [occur_meta ta] test removed for support of eelim/ecase but consequences + are unclear... if occur_meta ta then error "cannot find a type for the generalisation" - else if occur_meta a then lambda_name env (na,ta,t) + else *) if occur_meta a then lambda_name env (na,ta,t) else lambda_name env (na,ta,subst_term_occ locc a t)) c (List.rev l) lname_typ -let abstract_list_all env sigma typ c l = - let ctxt,_ = decomp_n_prod env sigma (List.length l) typ in +let abstract_list_all env evd typ c l = + let ctxt,_ = decomp_n_prod env (evars_of evd) (List.length l) typ in let p = abstract_scheme env c (List.map (function a -> [],a) l) ctxt in try - if is_conv_leq env sigma (Typing.type_of env sigma p) typ then p + if is_conv_leq env (evars_of evd) (Typing.mtype_of env evd p) typ then p else error "abstract_list_all" with UserError _ -> raise (PretypeError (env,CannotGeneralize typ)) @@ -576,11 +578,10 @@ let w_unify_to_subterm_list env mod_delta allow_K oplist t evd = (evd,[]) let secondOrderAbstraction env mod_delta allow_K typ (p, oplist) evd = - let sigma = evars_of evd in let (evd',cllist) = w_unify_to_subterm_list env mod_delta allow_K oplist typ evd in let typp = Typing.meta_type evd' p in - let pred = abstract_list_all env sigma typp typ cllist in + let pred = abstract_list_all env evd' typp typ cllist in w_unify_0 env topconv mod_delta (mkMeta p) pred evd' let w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd = diff --git a/pretyping/unification.mli b/pretyping/unification.mli index f163e95f6..d2cb20550 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -28,8 +28,8 @@ val w_unify_meta_types : env -> evar_defs -> evar_defs (*i This should be in another module i*) -(* [abstract_list_all env sigma t c l] *) +(* [abstract_list_all env evd t c l] *) (* abstracts the terms in l over c to get a term of type t *) (* (exported for inv.ml) *) val abstract_list_all : - env -> evar_map -> constr -> constr -> constr list -> constr + env -> evar_defs -> constr -> constr -> constr list -> constr |