diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-17 16:22:12 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-17 16:22:12 +0000 |
| commit | 02d299630b7436f634e667766a7b09624190cbf5 (patch) | |
| tree | 36b8af9f33f3011b8b6ef1d0b38ad7e988a9cd8a /contrib/extraction/mlutil.ml | |
| parent | 5fb1b9953d82fd6204e8a99845a0c0b145a0ff45 (diff) | |
reparation temporaire(?) a coup de MLdummy'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2895 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/mlutil.ml')
| -rw-r--r-- | contrib/extraction/mlutil.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 86de23302..5f954d776 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -206,7 +206,7 @@ let gen_subst v d t = let i'= i-n in if i' < 1 then a else if i' < Array.length v then - if v.(i') = 0 then MLdummy + if v.(i') = 0 then MLdummy' else MLrel (v.(i')+n) else MLrel (i+d) | a -> ast_map_lift subst n a @@ -817,7 +817,7 @@ let rec expunge_fix_decls prm v c b = function let rec optimize prm = function | [] -> [] - | (DdummyType r | Dterm(r,MLdummy)) as d :: l -> + | (DdummyType r | Dterm(r,MLdummy')) as d :: l -> if List.mem r prm.to_appear then d :: (optimize prm l) else optimize prm l | Dterm (r,t) :: l -> |