diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-16 14:33:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-16 14:38:51 +0100 |
| commit | f88cce2698da000ab9054da31330db70997a41a4 (patch) | |
| tree | 8bc74094c06411792ff1431c4ce73c77ec94bb2f /toplevel/metasyntax.ml | |
| parent | 5ba84979df97996cd04f44e506742bb58ecf0465 (diff) | |
Fixing CAMLP4 compilation.
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 85f8f61a8..6d6376de3 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -141,7 +141,7 @@ let extend_atomic_tactic name entries = | None -> () | Some args -> let body = Tacexpr.TacML (Loc.ghost, name, args) in - Tacenv.register_ltac false (Names.Id.of_string id) body + Tacenv.register_ltac false false (Names.Id.of_string id) body in List.iter add_atomic entries |