diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-14 20:32:27 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-14 20:32:27 +0000 |
| commit | 4fd92a741c0342fbbca1549281695e1ee92c1ba1 (patch) | |
| tree | 99da7bc0bc9b15c685889c91f8387bb5dfbba549 /parsing | |
| parent | 724ae6574aa7488f28fefec50fd25c3aa8aef97b (diff) | |
Restauration échappement ML
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3238 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/q_coqast.ml4 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 06ccc6bea..5a8258cb4 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -187,6 +187,8 @@ let mlexpr_of_red_flags { } >> let rec mlexpr_of_constr = function + | Topconstr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) -> + anti loc (string_of_id id) | Topconstr.CRef r -> <:expr< Topconstr.CRef $mlexpr_of_reference r$ >> | Topconstr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" | Topconstr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" |