diff options
Diffstat (limited to 'plugins/romega/ReflOmegaCore.v')
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index ab424c223..7e4475d40 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -1284,7 +1284,7 @@ Qed. (* Extraire une hypothèse de la liste *) Definition nth_hyps (n : nat) (l : hyps) := nth n l TrueTerm. - +Unset Printing Notations. Theorem nth_valid : forall (ep : list Prop) (e : list int) (i : nat) (l : hyps), interp_hyps ep e l -> interp_proposition ep e (nth_hyps i l). |