diff options
| author | msozeau | 2008-12-14 16:34:43 +0000 |
|---|---|---|
| committer | msozeau | 2008-12-14 16:34:43 +0000 |
| commit | c74f11d65b693207cdfa6d02f697e76093021be7 (patch) | |
| tree | b32866140d9f5ecde0bb719c234c6603d44037a8 /contrib/funind | |
| parent | 2f63108dccc104fe32344d88b35193d34a88f743 (diff) | |
Generalized binding syntax overhaul: only two new binders: `() and `{},
guessing the binding name by default and making all generalized
variables implicit. At the same time, continue refactoring of
Record/Class/Inductive etc.., getting rid of [VernacRecord]
definitively. The AST is not completely satisfying, but leaning towards
Record/Class as restrictions of inductive (Arnaud, anyone ?).
Now, [Class] declaration bodies are either of the form [meth : type] or
[{ meth : type ; ... }], distinguishing singleton "definitional" classes
and inductive classes based on records. The constructor syntax is
accepted ([meth1 : type1 | meth1 : type2]) but raises an error
immediately, as support for defining a class by a general inductive type
is not there yet (this is a bugfix!).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11679 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 62f1148320..67ae85d648 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -1370,7 +1370,7 @@ let do_build_inductive 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 ) + List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , None, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = @@ -1385,7 +1385,7 @@ let do_build_inductive 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 ) + List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , None, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = |