Backport code from command.ml to subtac_command.ml for definining

recursive definitions. Now program accepts cofixpoints and uses the new
way infer structurally decreasing arguments. Also, checks for correct
recursive calls before giving the definition to the obligations machine
(solves part 1 of bug #1784).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10529 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 9 insertions, 15 deletions

diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
index c2ee4595d0..ac49ca96a4 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/contrib/subtac/test/Mutind.v
@@ -1,10 +1,11 @@
 Require Import List.
+
 Program Fixpoint f a : { x : nat | x > 0 } := 
   match a with
   | 0 => 1
   | S a' => g a a'
   end
-with g a b { struct b } : { x : nat | x > 0 } := 
+with g a b : { x : nat | x > 0 } := 
   match b with
   | 0 => 1
   | S b' => f b'
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index a5a8b85f99..501aa79815 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -1,20 +1,17 @@
-Require Import Coq.subtac.Utils.
+Require Import Coq.Program.Program.
 Require Import Coq.Arith.Compare_dec.
 Notation "( x & y )" := (existS _ x y) : core_scope.
   
+Require Import Omega.
+
 Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf lt a}  :
   { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
   if le_lt_dec b a then let (q', r) := euclid (a - b) b in 
   (S q' & r)
   else (O & a).
 
-Require Import Omega.
-
-Obligations.
-Solve Obligations using subtac_simpl ; omega.
-
 Next Obligation.
-  assert(x0 * S q' = x0 * q' + x0) by auto with arith ; omega.
+  assert(b * S q' = b * q' + b) by auto with arith ; omega.
 Defined.
 
 Program Definition test_euclid : (prod nat nat) := let (q, r) := euclid 4 2 in (q, q).
diff --git a/contrib/subtac/test/measure.v b/contrib/subtac/test/measure.v
index 4764037d94..4f938f4f87 100644
--- a/contrib/subtac/test/measure.v
+++ b/contrib/subtac/test/measure.v
@@ -2,7 +2,7 @@ Notation "( x & y )" := (@existS _ _ x y) : core_scope.
 Unset Printing All.
 Require Import Coq.Arith.Compare_dec.
 
-Require Import Coq.subtac.Utils.
+Require Import Coq.Program.Program.
 
 Fixpoint size (a : nat) : nat :=
   match a with
@@ -10,15 +10,11 @@ Fixpoint size (a : nat) : nat :=
   | S n => S (size n)
   end.
 
-Program Fixpoint test_measure (a : nat) {measure a size}  : nat :=
+Program Fixpoint test_measure (a : nat) {measure size a}  : nat :=
   match a with
   | S (S n) => S (test_measure n)
-  | x => x
+  | 0 | S 0 => a
   end.
-subst.
-unfold n0.
-auto with arith.
-Qed.
 
 Check test_measure.
 Print test_measure.
\ No newline at end of file