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 /proofs/logic.ml | |
| parent | 84cbc09bd1400f732a6c70e8a840e4c13d018478 (diff) | |
Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 02f3a16d8..fb88b8754 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -382,10 +382,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm = match kind_of_term f with | Ind _ | Const _ when (isInd f || has_polymorphic_type (fst (destConst f))) -> + let sigma, ty = (* Sort-polymorphism of definition and inductive types *) - goalacc, - type_of_global_reference_knowing_conclusion env sigma f conclty, - sigma, f + type_of_global_reference_knowing_conclusion env sigma f conclty + in + goalacc, ty, sigma, f | _ -> mk_hdgoals sigma goal goalacc f in |