diff options
| author | William Lawvere | 2017-07-01 22:10:46 -0700 |
|---|---|---|
| committer | William Lawvere | 2017-07-01 22:10:46 -0700 |
| commit | 80649ebaba75838bfd28ae78822cd2c078da4b23 (patch) | |
| tree | ac29ab5edd3921dbee1c2256737347fd1542dc67 /API/API.ml | |
| parent | c2942e642ee6f83cc997f9a2510cdb7446a65cb4 (diff) | |
| parent | 35e0f327405fb659c7ec5f9f7d26ea284aa45810 (diff) | |
Merge remote-tracking branch 'upstream/trunk' into trunk
Diffstat (limited to 'API/API.ml')
| -rw-r--r-- | API/API.ml | 14 |
1 files changed, 1 insertions, 13 deletions
diff --git a/API/API.ml b/API/API.ml index 2b7bbd561b..29aa1b7a57 100644 --- a/API/API.ml +++ b/API/API.ml @@ -138,6 +138,7 @@ module Typeclasses = Typeclasses module Pretype_errors = Pretype_errors module Notation = Notation module Declarations = Declarations +module Univops = Univops module Declareops = Declareops module Globnames = Globnames module Environ = Environ @@ -200,16 +201,3 @@ module Entries = | ParameterEntry of parameter_entry | ProjectionEntry of projection_entry end - -(* NOTE: It does not make sense to replace the following "module expression" - simply with "module Proof_type = Proof_type" because - there is only "proofs/proof_type.mli"; - there is no "proofs/proof_type.ml" file *) -module Proof_type = - struct - type goal = Goal.goal - type tactic = goal Evd.sigma -> goal list Evd.sigma - type rule = Proof_type.prim_rule = - | Cut of bool * bool * Names.Id.t * Term.types - | Refine of Term.constr - end |