diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-17 09:28:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-17 09:28:28 +0200 |
| commit | c684d7621bbd0cb059aee0c47cd2de78ec518f30 (patch) | |
| tree | 58e6c0bba1855e810edd68f192421fe9ebb3bbc4 /grammar/tacextend.ml4 | |
| parent | 070fcb00f53062e8bbd57c9398d7a78eba12f641 (diff) | |
Fixing Camlp4 compilation
Diffstat (limited to 'grammar/tacextend.ml4')
| -rw-r--r-- | grammar/tacextend.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index dc8a47864..5a65fe93a 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -170,7 +170,7 @@ let declare_tactic loc s c cl = match cl with let name = <:expr< Libnames.Ident($dloc$, Names.Id.of_string $name$) >> in declare_str_items loc [ <:str_item< do { - let obj () = Tacenv.register_ltac false false [($name$, false, $body$)] in + let obj () = Tacenv.register_ltac False False [($name$, False, $body$)] in try do { Tacenv.register_ml_tactic $se$ $tac$; Mltop.declare_cache_obj obj __coq_plugin_name; } |