diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-04 14:48:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:23:49 +0100 |
| commit | d528fdaf12b74419c47698cca7c6f1ec762245a3 (patch) | |
| tree | 2edbaac4e19db595e0ec763de820cbc704897043 /pretyping/tacred.ml | |
| parent | 6bd193ff409b01948751525ce0f905916d7a64bd (diff) | |
Retyping API using EConstr.
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 357a80f44..ac2a3bc49 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -974,7 +974,7 @@ let matches_head env sigma c t = let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c = match kind_of_term c with | Proj (p, r) -> (* Treat specially for partial applications *) - let t = Retyping.expand_projection env sigma p r [] in + let t = Retyping.expand_projection env sigma p (EConstr.of_constr r) [] in let hdf, al = destApp t in let a = al.(Array.length al - 1) in let app = (mkApp (hdf, Array.sub al 0 (Array.length al - 1))) in @@ -1150,7 +1150,7 @@ let compute = cbv_betadeltaiota * the specified occurrences. *) let abstract_scheme env (locc,a) (c, sigma) = - let ta = Retyping.get_type_of env sigma a in + let ta = Retyping.get_type_of env sigma (EConstr.of_constr 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 |