- Correction bug highlighting "Module" dans Coqide

- Divers code mort (evarutil.ml, Bvector.v)
- MAJ perf-analysis



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

5 files changed, 17 insertions, 122 deletions

diff --git a/dev/doc/perf-analysis b/dev/doc/perf-analysis
index 411cb61cc..8e4815447 100644
--- a/dev/doc/perf-analysis
+++ b/dev/doc/perf-analysis
@@ -1,17 +1,23 @@
 Performance analysis (trunk repository)
 ---------------------------------------
 
+May 21, 2008: New version of CoRN
+  (needs +84% more time to compile)
+
+Apr 25-29, 2008: Temporary attempt with delta in eauto (Matthieu)
+  (+28% CoRN) 
+
 Apr 17, 2008: improvement probably due to commit 10807 or 10813 (bug
   fixes, control of zeta in rewrite, auto (??))
   (-18% Buchberger, -40% PAutomata, -28% IntMap, -43% CoRN, -13% LinAlg,
   but CatsInZFC -0.5% only, PiCalc stable, PersistentUnionFind -1%)
 
 Mar 11, 2008:
-  (+19 % PersistentUnionFind wrt Mar 3, +21% Angles, 
+  (+19% PersistentUnionFind wrt Mar 3, +21% Angles, 
    +270% Continuations between 7/3 and 18/4)
 
 Mar 7, 2008:
-  (-10 % PersistentUnionFind wrt Mar 3)
+  (-10% PersistentUnionFind wrt Mar 3)
 
 Feb 20, 2008: temporary 1-day slow down
   (+64% LinAlg)
diff --git a/ide/highlight.mll b/ide/highlight.mll
index c01ec1a81..43b257977 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -71,7 +71,7 @@ let identchar =
 let ident = firstchar identchar*
 
 let multiword_declaration =
-  "Module" (space+ "Type")
+  "Module" (space+ "Type")?
 | "Program" space+ ident
 | "Existing" space+ "Instance"
 | "Canonical" space+ "Structure"
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 6bcf22665..e0ed5be55 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -280,58 +280,6 @@ let evar_well_typed_body evd ev evi body =
        print_constr body);
     false
 
-(* Unused
-
-let strict_inverse = false
-
-let inverse_instance env evd ev evi inst rhs =
-  let subst = make_projectable_subst (evars_of evd) evi inst in
-  let subst = List.map (fun (x,(_,y)) -> (y,mkVar x)) subst in
-  let evdref = ref evd in
-  let error () = 
-    error_not_clean env (evars_of !evdref) ev rhs (evar_source ev !evdref) in
-  let rec subs rigid k t =
-    match kind_of_term t with
-      | Rel i ->
- 	  if i<=k then t
- 	  else
-            (try List.assoc (mkRel (i-k)) subst
-             with Not_found ->
-               if rigid then error()
-               else if strict_inverse then
-                 failwith "cannot solve pb yet"
-               else t)
-      | Var id ->
-          (try List.assoc t subst
-           with Not_found ->
-             if rigid then error()
-             else if
-               not strict_inverse &&
-               List.exists (fun (id',_,_) -> id=id') (evar_context evi)
-             then
-               failwith "cannot solve pb yet"
-             else t)
-      | Evar (evk,args as ev) ->
-          if Evd.is_defined_evar !evdref ev then
-            subs rigid k (existential_value (evars_of !evdref) ev)
-          else
-	    let args' = Array.map (subs false k) args in
-	    mkEvar (evk,args')
-      | _ -> map_constr_with_binders succ (subs rigid) k t in
-  let body = subs true 0 (nf_evar (evars_of evd) rhs) in
-  (!evdref,body)
-
-
-let is_defined_equation env evd (ev,inst) rhs =
-  is_pattern inst &&
-  not (occur_evar ev rhs) &&
-  try
-    let evi = Evd.find (evars_of evd) ev in
-    let (evd',body) = inverse_instance env evd ev evi inst rhs in
-    evar_well_typed_body evd' ev evi body
-  with Failure _ -> false
-*)
-
 (* We have x1..xq |- ?e1 and had to solve something like 
  * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some 
  * ?e2[v1..vn], hence flexible. We had to go through k binders and now 
diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v
index d50f545da..60c2e6579 100644
--- a/test-suite/ide/undo.v
+++ b/test-suite/ide/undo.v
@@ -4,7 +4,7 @@
 (* Undoing arbitrary commands, as first step *)
 
 Theorem a : O=O.
-Set Printing All.
+Ltac f x := x.
 assert True by trivial.
 trivial.
 Qed.
@@ -13,7 +13,7 @@ Qed.
 
 Theorem b : O=O.
 assert True by trivial.
-Set Printing All.
+Ltac g x := x.
 assert True by trivial.
 trivial.
 Qed.
@@ -65,7 +65,7 @@ Qed.
 Theorem n : O=O.
 assert True by trivial.
 Definition o := O.
-Set Printing All.
+Ltac h x := x.
 assert True by trivial.
 Focus.
 Definition p := O.
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index e48dd9a5b..9dbd90f05 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -72,55 +72,6 @@ Proof.
   exact (f H0).
 Defined.
 
-(* This works...
-
-Notation "'!rew' a -> b [ Heq ]  'in' t" := (eq_rect a _ t b Heq)
-  (at level 10, a, b at level 80).
-
-Fixpoint Vlast (n:nat) (v:vector (S n)) { struct v } : A :=
-  match v with
-  | Vnil => I
-  | Vcons a n v => 
-      match v in vector q return n=q -> A with
-      | Vnil => fun _ => a
-      | Vcons _ q _ => fun Heq => Vlast q (!rew n -> (S q) [Heq] in v)
-      end (refl_equal n)
-  end.
-*)
-
-(* Remarks on the definition of Vlast...
-
-(* The ideal version... still now accepted, even with Program *)
-Fixpoint Vlast (n:nat) (v:vector (S n)) { struct v } : A :=
-  match v with
-  | Vnil => I
-  | Vcons a _ Vnil => a
-  | Vcons a n v => Vlast (pred n) v
-  end.
-
-(* This version does not work because Program Fixpoint expands v with
-   violates the guard condition *)
-
-Program Fixpoint Vlast (n:nat) (v:vector (S n)) { struct v } : A :=
-  match v in vector p return match p with O => True | _ => A end with
-  | Vnil => I
-  | Vcons a _ Vnil => a
-  | Vcons a _ (Vcons _ n _ as v) => Vlast n v
-  end.
-
-(* This version works *)
-
-Program Fixpoint Vlast (n:nat) (v:vector (S n)) { struct v } : A :=
-  match v in vector p return match p with O => True | _ => A end with
-  | Vnil => I
-  | Vcons a n v =>
-      match v with
-      | Vnil => a
-      | Vcons _ q _ => Vlast q v
-      end
-  end.
-*)
-
 Fixpoint Vconst (a:A) (n:nat) :=
   match n return vector n with
   | O => Vnil
@@ -192,15 +143,6 @@ Fixpoint Vunary n (v:vector n) : vector n :=
 
 Variable g : A -> A -> A.
 
-(* Would need to have the constraint n = n' ...
-
-Fixpoint Vbinary n (v w:vector n) : vector n :=
-  match v, w with
-  | Vnil, Vnil => Vnil
-  | Vcons a n' v', Vcons b _ w' => Vcons (g a b) n' (Vbinary n' v' w')
-  end.
-*)
-
 Lemma Vbinary : forall n:nat, vector n -> vector n -> vector n.
 Proof.
   induction n as [| n h]; intros v v0.
@@ -212,12 +154,11 @@ Defined.
 
 (** Eta-expansion of a vector *)
 
-Definition Vid : forall n:nat, vector n -> vector n.
-Proof.
-  destruct n; intro v.
-  exact Vnil.
-  exact (Vcons (Vhead _ v) _ (Vtail _ v)).
-Defined.
+Definition Vid n : vector n -> vector n :=
+  match n with
+  | O => fun _ => Vnil
+  | _ => fun v => Vcons (Vhead _ v) _ (Vtail _ v)
+  end.
 
 Lemma Vid_eq : forall (n:nat) (v:vector n), v = Vid n v.
 Proof.