diff options
| author | herbelin | 2006-03-22 09:41:17 +0000 |
|---|---|---|
| committer | herbelin | 2006-03-22 09:41:17 +0000 |
| commit | 8291c83620312550d1ccbe9a304fd43f35724b12 (patch) | |
| tree | e5a19f90598a1f15bed7462d081bce333c7d22e8 /interp | |
| parent | 8fb0925c056c3e9a6103355eed31d283d6498070 (diff) | |
- Correction bug calcul mind_consnrealargs, introduit à la révision
7833, et que la révision 8644 n'avait pas corrigé dans le bon sens;
renommage en mind_consnrealdecls pour éviter la confusion de sens
avec mind_nrealargs
- Correction de la description du type one_inductive_body
- Ajout test avec let-in dans params et dans type constructeur
(fichier Case12.v)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8653 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0fe01799e1..fcdd0a786e 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -904,7 +904,7 @@ let rec raw_of_pat env = function let mib,mip = lookup_mind_specif (Global.env()) ind in let k = mip.Declarations.mind_nrealargs in let nparams = mib.Declarations.mind_nparams in - let cstrnargs = mip.Declarations.mind_consnrealargs in + let cstrnargs = mip.Declarations.mind_consnrealdecls in Detyping.detype_case false (raw_of_pat env) (raw_of_eqns env) (fun _ _ -> false (* lazy: don't try to display pattern with "if" *)) avoid (ind,cs,nparams,cstrnargs,k) typopt tm bv |