aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/doc/perf-analysis10
-rw-r--r--ide/highlight.mll2
-rw-r--r--pretyping/evarutil.ml52
-rw-r--r--test-suite/ide/undo.v6
-rw-r--r--theories/Bool/Bvector.v69
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 10:50:45 +0000