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/interface | |
| 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/interface')
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 4 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 26 |
2 files changed, 15 insertions, 15 deletions
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index f41d88bd60..d6ef1ea3b6 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -107,9 +107,9 @@ let convert_one_inductive sp tyi = let env = Global.env () in let envpar = push_rel_context params env in let sp = sp_of_global (IndRef (sp, tyi)) in - (((dummy_loc,basename sp), + (((false,(dummy_loc,basename sp)), convert_env(List.rev params), - Some (extern_constr true envpar arity), + Some (extern_constr true envpar arity), None, Constructors (convert_constructors envpar cstrnames cstrtypes)), None);; (* This function converts a Mutual inductive definition to a Coqast.t. diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index b404478ffb..6d6a0c0656 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1969,22 +1969,22 @@ let rec xlate_vernac = translated_restriction) | SearchAbout [] -> assert false) - | (*Record from tactics/Record.v *) - VernacRecord - (_, (add_coercion, (_,s)), binders, c1, - rec_constructor_or_none, field_list) -> - let record_constructor = - xlate_ident_opt (Option.map snd rec_constructor_or_none) in - CT_record - ((if add_coercion then CT_coercion_atm else - CT_coerce_NONE_to_COERCION_OPT(CT_none)), - xlate_ident s, xlate_binder_list binders, - xlate_formula (Option.get c1), record_constructor, - build_record_field_list field_list) +(* | (\*Record from tactics/Record.v *\) *) +(* VernacRecord *) +(* (_, (add_coercion, (_,s)), binders, c1, *) +(* rec_constructor_or_none, field_list) -> *) +(* let record_constructor = *) +(* xlate_ident_opt (Option.map snd rec_constructor_or_none) in *) +(* CT_record *) +(* ((if add_coercion then CT_coercion_atm else *) +(* CT_coerce_NONE_to_COERCION_OPT(CT_none)), *) +(* xlate_ident s, xlate_binder_list binders, *) +(* xlate_formula (Option.get c1), record_constructor, *) +(* build_record_field_list field_list) *) | VernacInductive (isind, lmi) -> let co_or_ind = if isind then "Inductive" else "CoInductive" in let strip_mutind = function - (((_,s), parameters, c, Constructors constructors), notopt) -> + (((_, (_,s)), parameters, c, _, Constructors constructors), notopt) -> CT_ind_spec (xlate_ident s, xlate_binder_list parameters, xlate_formula (Option.get c), build_constructors constructors, |