diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-06-03 10:28:40 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-06-03 10:28:40 +0000 |
| commit | e860dcf1df4d7042aa872ba4ad914d1d64d574cf (patch) | |
| tree | ccaea77ed45e472307e5b3c9023aebfbb0d6dff9 /toplevel/vernacexpr.ml | |
| parent | 3eb35bf30c52aad878867650a233744b7028a62d (diff) | |
Intgration uniforme de coercions dans les dclarations (Variable and co) et retouche des Record
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2747 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/vernacexpr.ml')
| -rw-r--r-- | toplevel/vernacexpr.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 365192599..f1bd6ed52 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -140,12 +140,13 @@ type inductive_flag = bool (* true = Inductive; false = CoInductive *) type sort_expr = t -type simple_binders = identifier * constr_ast -type constructor_expr = identifier * coercion_flag * constr_ast +type simple_binder = identifier * constr_ast +type 'a with_coercion = coercion_flag * 'a +type constructor_expr = simple_binder with_coercion type inductive_expr = - identifier * simple_binders list * constr_ast * constructor_expr list + identifier * simple_binder list * constr_ast * constructor_expr list type fixpoint_expr = - identifier * simple_binders list * constr_ast * constr_ast + identifier * simple_binder list * constr_ast * constr_ast type cofixpoint_expr = identifier * constr_ast * constr_ast @@ -180,15 +181,15 @@ type vernac_expr = constr_ast * bool * Proof_type.declaration_hook | VernacEndProof of opacity_flag * (identifier * theorem_kind option) option | VernacExactProof of constr_ast - | VernacAssumption of assumption_kind * simple_binders list + | VernacAssumption of assumption_kind * simple_binder with_coercion list | VernacInductive of inductive_flag * inductive_expr list | VernacFixpoint of fixpoint_expr list | VernacCoFixpoint of cofixpoint_expr list | VernacScheme of (identifier * bool * qualid located * sort_expr) list (* Gallina extensions *) - | VernacRecord of coercion_flag * identifier * simple_binders list - * sort_expr * identifier option * (coercion_flag * local_decl_expr) list + | VernacRecord of identifier with_coercion * simple_binder list + * sort_expr * identifier option * local_decl_expr with_coercion list | VernacBeginSection of identifier | VernacEndSection of identifier | VernacRequire of |