diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 38 | ||||
| -rw-r--r-- | proofs/clenv.mli | 21 |
2 files changed, 10 insertions, 49 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index bc6da8c347..b75c675297 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -83,6 +83,16 @@ let clenv_push_prod cl = (* Instantiate the first [bound] products of [t] with metas (all products if [bound] is [None]; unfold local defs *) +(** [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where + [lmetas] is a list of metas to be applied to a proof of [t] so that + it produces the unification pattern [ccl]; [sigma'] is [sigma] + extended with [lmetas]; if [n] is defined, it limits the size of + the list even if [ccl] is still a product; otherwise, it stops when + [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x] + and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and + [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1] + and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *) + let clenv_environments evd bound t = let rec clrec (e,metas) n t = match n, kind_of_term t with @@ -100,34 +110,6 @@ let clenv_environments evd bound t = in clrec (evd,[]) bound t -(* Instantiate the first [bound] products of [t] with evars (all products if - [bound] is [None]; unfold local defs *) - -let clenv_environments_evars env evd bound t = - let rec clrec (e,ts) n t = - match n, kind_of_term t with - | (Some 0, _) -> (e, List.rev ts, t) - | (n, Cast (t,_,_)) -> clrec (e,ts) n t - | (n, Prod (na,t1,t2)) -> - let e',constr = Evarutil.new_evar e env t1 in - let dep = dependent (mkRel 1) t2 in - clrec (e', constr::ts) (Option.map ((+) (-1)) n) - (if dep then (subst1 constr t2) else t2) - | (n, LetIn (na,b,_,t)) -> clrec (e,ts) n (subst1 b t) - | (n, _) -> (e, List.rev ts, t) - in - clrec (evd,[]) bound t - -let clenv_conv_leq env sigma t c bound = - let ty = Retyping.get_type_of env sigma c in - let evd = Evd.create_goal_evar_defs sigma in - let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in - let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in - let evars = Evarconv.consider_remaining_unif_problems env evars in - let args = List.map (whd_evar evars) args in - check_evars env sigma evars (applist (c,args)); - args - let mk_clenv_from_env environ sigma n (c,cty) = let evd = create_goal_evar_defs sigma in let (evd,args,concl) = clenv_environments evd n cty in diff --git a/proofs/clenv.mli b/proofs/clenv.mli index bfb5ee27ca..c8b63ea0fd 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -109,27 +109,6 @@ val make_clenv_binding_apply : val make_clenv_binding : Goal.goal sigma -> constr * constr -> constr bindings -> clausenv -(** [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where - [lmetas] is a list of metas to be applied to a proof of [t] so that - it produces the unification pattern [ccl]; [sigma'] is [sigma] - extended with [lmetas]; if [n] is defined, it limits the size of - the list even if [ccl] is still a product; otherwise, it stops when - [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x] - and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and - [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1] - and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *) -val clenv_environments : - evar_map -> int option -> types -> evar_map * constr list * types - -(** [clenv_environments_evars env sigma n t] does the same but returns - a list of Evar's defined in [env] and extends [sigma] accordingly *) -val clenv_environments_evars : - env -> evar_map -> int option -> types -> evar_map * constr list * types - -(** [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *) -val clenv_conv_leq : - env -> evar_map -> types -> constr -> int -> constr list - (** if the clause is a product, add an extra meta for this product *) exception NotExtensibleClause val clenv_push_prod : clausenv -> clausenv |