diff options
| author | barras | 2001-05-03 09:54:17 +0000 |
|---|---|---|
| committer | barras | 2001-05-03 09:54:17 +0000 |
| commit | bf352b0b29a8e3d55eaa986c4f493af48f8ddf52 (patch) | |
| tree | b0633f3a1ee73bd685327c2c988426d65de7a58a /contrib/ring | |
| parent | c4a517927f148e0162d22cb7077fa0676d799926 (diff) | |
Changement de la structure des points fixes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/ring')
| -rw-r--r-- | contrib/ring/quote.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index e4297ce85e..7908af7ecd 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -226,7 +226,7 @@ let compute_ivs gl f cs = let cst = try destConst f with _ -> i_can't_do_that () in let body = constant_value (Global.env()) cst in match decomp_term body with - | IsFix(([| len |], 0), ([| typ |], [ name ], [| body2 |])) -> + | IsFix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) -> let (args3, body3) = decompose_lam body2 in let nargs3 = List.length args3 in begin match decomp_term body3 with |