From 1674ab8bc0b76a1162928d0d9097c6a97486205d Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 14 Mar 2012 09:52:07 +0000 Subject: Remove support for "abstract typing constraints" that requires unicity of solutions to unification. Only allow bidirectional checking of constructor applications, enabled by a program_mode flag: it is backwards-incompatible due to delta-reduction, constructor parameters might get instantiated with delta-equivalent but not syntactically equivalent terms. Prepare for merging the Program-specific version of Pretyping/Cases/Coercion with the main code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15032 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Vectors/Fin.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/Vectors') diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v index a5e37f34b..717139a0a 100644 --- a/theories/Vectors/Fin.v +++ b/theories/Vectors/Fin.v @@ -78,8 +78,8 @@ end. (** [to_nat f] = p iff [f] is the p{^ th} element of [fin m]. *) Fixpoint to_nat {m} (n : t m) : {i | i < m} := - match n in t k return {i | i< k} with - |F1 j => exist (fun i => i< S j) 0 (Lt.lt_0_Sn j) + match n with + |F1 j => exist _ 0 (Lt.lt_0_Sn j) |FS _ p => match to_nat p with |exist i P => exist _ (S i) (Lt.lt_n_S _ _ P) end end. @@ -87,7 +87,7 @@ Fixpoint to_nat {m} (n : t m) : {i | i < m} := p >= n else *) Fixpoint of_nat (p n : nat) : (t n) + { exists m, p = n + m } := match n with - |0 => inright _ (ex_intro (fun x => p = 0 + x) p (@eq_refl _ p)) + |0 => inright _ (ex_intro _ p eq_refl) |S n' => match p with |0 => inleft _ (F1) |S p' => match of_nat p' n' with -- cgit v1.2.3