diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-05 18:45:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:23:51 +0100 |
| commit | 83607f75a13ea915affa8cfc5bfc14cc944c61ef (patch) | |
| tree | da0c80b672a6929c9d8a01bb9589bc68a28f03b1 /pretyping/tacred.ml | |
| parent | 214a2ffd2cce3fa24908710af7db528a40345db6 (diff) | |
Find_subterm API using EConstr.
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index c1e9573d2..290d77b1b 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1150,13 +1150,14 @@ let compute = cbv_betadeltaiota * the specified occurrences. *) let abstract_scheme env (locc,a) (c, sigma) = - let ta = Retyping.get_type_of env sigma (EConstr.of_constr a) in + let a = EConstr.of_constr a in + let ta = Retyping.get_type_of env sigma a in let na = named_hd env ta Anonymous in if occur_meta sigma (EConstr.of_constr ta) then error "Cannot find a type for the generalisation."; - if occur_meta sigma (EConstr.of_constr a) then + if occur_meta sigma a then mkLambda (na,ta,c), sigma else - let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in + let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a (EConstr.of_constr c) in mkLambda (na,ta,c'), sigma' let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c -> |