diff options
| author | aspiwack | 2008-11-05 16:45:18 +0000 |
|---|---|---|
| committer | aspiwack | 2008-11-05 16:45:18 +0000 |
| commit | 9fe895d340a2a578d682c077b66e7a3171d31c87 (patch) | |
| tree | 4652a4e854bfdb5bead06c74b5862d0708230730 /contrib | |
| 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')
| -rw-r--r-- | contrib/funind/merge.ml | 2 | ||||
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 14 |
2 files changed, 13 insertions, 3 deletions
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml index ec456aae6f..b7cee73902 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 diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 7534ce2ca7..48a96f8b6c 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -1226,9 +1226,14 @@ let do_build_inductive | UserError(s,msg) as e -> let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) + let repacked_rel_inds = + List.map (fun ((a , b , c , l),ntn) -> (a , b, c , Vernacexpr.Constructors l),ntn ) + rel_inds + in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++ + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,repacked_rel_inds)) + ++ fnl () ++ msg in observe (msg); @@ -1236,9 +1241,14 @@ let do_build_inductive | e -> let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) + let repacked_rel_inds = + List.map (fun ((a , b , c , l),ntn) -> (a , b, c , Vernacexpr.Constructors l),ntn ) + rel_inds + in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++ + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,repacked_rel_inds)) + ++ fnl () ++ Cerrors.explain_exn e in observe msg; |