diff options
Diffstat (limited to 'contrib/subtac/subtac.ml')
| -rw-r--r-- | contrib/subtac/subtac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index c144f1f9e..4433239f3 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -158,7 +158,7 @@ let start_proof_and_print env isevars idopt k t hook = let subtac (loc, command) = check_required_library ["Coq";"Init";"Datatypes"]; check_required_library ["Coq";"Init";"Specif"]; - check_required_library ["Coq";"Logic";"JMeq"]; + (* check_required_library ["Coq";"Logic";"JMeq"]; *) require_library "Coq.subtac.FixSub"; require_library "Coq.subtac.Utils"; Subtac_obligations.set_default_tactic |