diff options
| author | barras | 2001-10-09 16:40:03 +0000 |
|---|---|---|
| committer | barras | 2001-10-09 16:40:03 +0000 |
| commit | f1778f0e830c50aaec250916f14e202d95960414 (patch) | |
| tree | ae220556180dfa55d6b638467deb7edf58d4c17b /contrib/ring | |
| parent | 8dbab7f463cabfc2913ab8615973c96ac98bf371 (diff) | |
Suppression des arguments sur les constantes, inductifs et constructeurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/ring')
| -rw-r--r-- | contrib/ring/quote.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 10ca06b78e..b87ec5861f 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -200,9 +200,9 @@ let decomp_term c = kind_of_term (strip_outer_cast c) let compute_lhs typ i nargsi = match kind_of_term typ with - | IsMutInd((sp,0),args) -> + | IsMutInd(sp,0) -> let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in - mkApp (mkMutConstruct (((sp,0),i+1), args), argsi) + mkApp (mkMutConstruct ((sp,0),i+1), argsi) | _ -> i_can't_do_that () (*s This function builds the pattern from the RHS. Recursive calls are |