diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-24 23:08:09 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-24 23:08:09 +0000 |
| commit | a2669e5c949d39cb4c05549cbcf405db65249285 (patch) | |
| tree | 4bc1159ef1f1dbb55d9bfbfcc565472e2bada4a7 /contrib | |
| parent | e3038e0822548b90792903ccb460a0e61f1cadaf (diff) | |
Remplacement de Syntactic Definition par Notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3267 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/romega/ReflOmegaCore.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v index 0df34f422..f4eea6c2f 100644 --- a/contrib/romega/ReflOmegaCore.v +++ b/contrib/romega/ReflOmegaCore.v @@ -50,7 +50,7 @@ Inductive proposition : Set := | NeqTerm: term -> term -> proposition. (* Définition des hypothèses *) -Syntactic Definition hyps := (list proposition). +Notation hyps := (list proposition). Definition absurd := (cons FalseTerm (nil proposition)). @@ -413,7 +413,7 @@ Save. (* \subsubsection{Généralisation à des listes de buts (disjonctions)} *) -Syntactic Definition lhyps := (list hyps). +Notation lhyps := (list hyps). Fixpoint interp_list_hyps [env: (list Z); l : lhyps] : Prop := Cases l of @@ -1778,7 +1778,7 @@ Inductive t_omega : Set := | O_NEGATE_CONTRADICT_INV : nat -> nat -> nat -> t_omega | O_STATE : Z -> step -> nat -> nat -> t_omega -> t_omega. -Syntactic Definition singleton := [a: hyps] (cons a (nil hyps)). +Notation singleton := [a: hyps] (cons a (nil hyps)). Fixpoint execute_omega [t: t_omega] : hyps -> lhyps := [l : hyps] Cases t of |