diff options
| author | herbelin | 2004-03-12 21:18:20 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-12 21:18:20 +0000 |
| commit | 9cfb9baa8b49e1fcc4f97fe63a328304baec259d (patch) | |
| tree | 8a5b254736c16c11f3ae1c194ab35ab947ea3258 | |
| parent | 803ebd5ff5cc46f87b16103e2fee3243887e88d2 (diff) | |
Bug inversion abstract_constr_expr et prod_constr_expr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5471 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | translate/ppconstrnew.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 2825344e45..753ac89ddf 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -626,8 +626,8 @@ let rec strip_context n iscast t = let transf istype env iscast bl c = let c' = - if istype then abstract_constr_expr c bl - else prod_constr_expr c bl in + if istype then prod_constr_expr c bl + else abstract_constr_expr c bl in if Options.do_translate() then let r = Constrintern.for_grammar |