From a2669e5c949d39cb4c05549cbcf405db65249285 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 24 Nov 2002 23:08:09 +0000 Subject: Remplacement de Syntactic Definition par Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3267 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/romega/ReflOmegaCore.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'contrib') 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 -- cgit v1.2.3