diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-10-28 14:08:46 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:54 +0200 |
| commit | 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 (patch) | |
| tree | 9e83ae395173699a7c5b6f00648c4336bedb7afd /pretyping/retyping.ml | |
| parent | 84cbc09bd1400f732a6c70e8a840e4c13d018478 (diff) | |
Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 31487125a..ccb9420fd 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -190,7 +190,7 @@ let retype ?(polyprop=true) sigma = with Reduction.NotArity -> retype_error NotAnArity) | Const cst -> let t = constant_type_in env cst in - (try Typeops.type_of_constant_knowing_parameters env t argtyps + (try Typeops.type_of_constant_type_knowing_parameters env t argtyps with Reduction.NotArity -> retype_error NotAnArity) | Var id -> type_of_var env id | Construct cstr -> type_of_constructor env cstr @@ -211,13 +211,13 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = match kind_of_term c with | Ind (ind,u) -> let spec = Inductive.lookup_mind_specif env ind in - type_of_inductive_knowing_conclusion env (spec,u) conclty + type_of_inductive_knowing_conclusion env sigma (spec,u) conclty | Const cst -> let t = constant_type_in env cst in (* TODO *) - Typeops.type_of_constant_knowing_parameters env t [||] - | Var id -> type_of_var env id - | Construct cstr -> type_of_constructor env cstr + sigma, Typeops.type_of_constant_type_knowing_parameters env t [||] + | Var id -> sigma, type_of_var env id + | Construct cstr -> sigma, type_of_constructor env cstr | _ -> assert false (* Profiling *) |