diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:35 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:35 +0200 |
| commit | e4282ea99c664d8d58067bee199cbbcf881b60d5 (patch) | |
| tree | d4c4a873eb055c728666f367469fa26c3417793a /dev | |
| parent | a0a94c1340a63cdb824507b973393882666ba52a (diff) | |
Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/base_include b/dev/base_include index d4366843..711dcb2a 100644 --- a/dev/base_include +++ b/dev/base_include @@ -14,6 +14,9 @@ #directory "tactics";; #directory "translate";; +#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *) +#directory "+camlp5";; (* Gramext is found in top_printers.ml *) + #use "top_printers.ml";; #use "vm_printers.ml";; @@ -112,6 +115,9 @@ open Proof_type open Redexpr open Refiner open Tacmach +open Decl_proof_instr +open Tactic_debug +open Decl_mode open Auto open Autorewrite |