diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-11-05 16:45:18 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-11-05 16:45:18 +0000 |
| commit | 9fe895d340a2a578d682c077b66e7a3171d31c87 (patch) | |
| tree | 4652a4e854bfdb5bead06c74b5862d0708230730 /contrib/funind/merge.ml | |
| parent | 7b16711f9f820b0bd1761b45f636852146f60cb4 (diff) | |
Nouvelle syntaxe pour écrire des records (co)inductifs :
CoInductive stream (A:Type) := { hd : A ; tl : stream A }.
Inductive nelist (A:Type) := { hd : A ; tl : option (nelist A) }.
L'affichage n'est pas encore poli. Il reste à choisir l'exact destin de
la syntaxe qui était apparue dans la 8.2beta pour les records
coinductifs (qui consistait à utiliser "Record" au lieu de "CoInductive"
comme maintenant).
VernacRecord et VernacInductive semblent maintenant faire doublon, il
doit y avoir moyen de les fusionner.
Les records mutuellement inductifs restent aussi à faire.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11539 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/funind/merge.ml')
| -rw-r--r-- | contrib/funind/merge.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml index ec456aae6..b7cee7390 100644 --- a/contrib/funind/merge.ml +++ b/contrib/funind/merge.ml @@ -855,7 +855,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = [rawlist], named ident. FIXME: params et cstr_expr (arity) *) let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift - (rawlist:(identifier * rawconstr) list):inductive_expr = + (rawlist:(identifier * rawconstr) list) = let lident = dummy_loc, shift.ident in let bindlist , cstr_expr = (* params , arities *) merge_rec_params_and_arity prms1 prms2 shift mkSet in |