diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-19 01:59:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:28:57 +0100 |
| commit | 7b43de20a4acd7c9da290f038d9a16fe67eccd59 (patch) | |
| tree | 14c110655c1a056c1f08557d7ffd3b0196012b3f /pretyping/retyping.ml | |
| parent | db252cb87e9c63f400fd4fddd2d771df3160d592 (diff) | |
Leminv API using EConstr.
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 6f03fc462..88899e633 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -123,7 +123,7 @@ let retype ?(polyprop=true) sigma = with Not_found -> retype_error BadRecursiveType in let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in - let t = EConstr.of_constr (betazetaevar_applist sigma n p (List.map EConstr.of_constr realargs)) in + let t = EConstr.of_constr (betazetaevar_applist sigma n p realargs) in (match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma (type_of env t))) with | Prod _ -> EConstr.of_constr (whd_beta sigma (applist (t, [c]))) | _ -> t) |