summaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/ExtrOcamlNatInt.v14
-rw-r--r--plugins/extraction/ExtrOcamlZInt.v32
-rw-r--r--plugins/extraction/extraction.ml36
-rw-r--r--plugins/extraction/modutil.ml60
-rw-r--r--plugins/funind/glob_term_to_relation.ml17
-rw-r--r--plugins/romega/ReflOmegaCore.v117
-rw-r--r--plugins/subtac/subtac_obligations.ml1
7 files changed, 138 insertions, 139 deletions
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
index fd134899..956ece79 100644
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ b/plugins/extraction/ExtrOcamlNatInt.v
@@ -14,6 +14,10 @@ Require Import ExtrOcamlBasic.
(** Disclaimer: trying to obtain efficient certified programs
by extracting [nat] into [int] is definitively *not* a good idea:
+ - This is just a syntactic adaptation, many things can go wrong,
+ such as name captures (e.g. if you have a constant named "int"
+ in your development, or a module named "Pervasives"). See bug #2878.
+
- Since [int] is bounded while [nat] is (theoretically) infinite,
you have to make sure by yourself that your program will not
manipulate numbers greater than [max_int]. Otherwise you should
@@ -34,17 +38,17 @@ Require Import ExtrOcamlBasic.
(** Mapping of [nat] into [int]. The last string corresponds to
a [nat_case], see documentation of [Extract Inductive]. *)
-Extract Inductive nat => int [ "0" "succ" ]
+Extract Inductive nat => int [ "0" "Pervasives.succ" ]
"(fun fO fS n -> if n=0 then fO () else fS (n-1))".
(** Efficient (but uncertified) versions for usual [nat] functions *)
Extract Constant plus => "(+)".
-Extract Constant pred => "fun n -> max 0 (n-1)".
-Extract Constant minus => "fun n m -> max 0 (n-m)".
+Extract Constant pred => "fun n -> Pervasives.max 0 (n-1)".
+Extract Constant minus => "fun n m -> Pervasives.max 0 (n-m)".
Extract Constant mult => "( * )".
-Extract Inlined Constant max => max.
-Extract Inlined Constant min => min.
+Extract Inlined Constant max => "Pervasives.max".
+Extract Inlined Constant min => "Pervasives.min".
(*Extract Inlined Constant nat_beq => "(=)".*)
Extract Inlined Constant EqNat.beq_nat => "(=)".
Extract Inlined Constant EqNat.eq_nat_decide => "(=)".
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
index c8c40e73..ab634329 100644
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ b/plugins/extraction/ExtrOcamlZInt.v
@@ -34,12 +34,12 @@ Extract Inductive N => int [ "0" "" ]
(** Efficient (but uncertified) versions for usual functions *)
Extract Constant Pos.add => "(+)".
-Extract Constant Pos.succ => "succ".
-Extract Constant Pos.pred => "fun n -> max 1 (n-1)".
-Extract Constant Pos.sub => "fun n m -> max 1 (n-m)".
+Extract Constant Pos.succ => "Pervasives.succ".
+Extract Constant Pos.pred => "fun n -> Pervasives.max 1 (n-1)".
+Extract Constant Pos.sub => "fun n m -> Pervasives.max 1 (n-m)".
Extract Constant Pos.mul => "( * )".
-Extract Constant Pos.min => "min".
-Extract Constant Pos.max => "max".
+Extract Constant Pos.min => "Pervasives.min".
+Extract Constant Pos.max => "Pervasives.max".
Extract Constant Pos.compare =>
"fun x y -> if x=y then Eq else if x<y then Lt else Gt".
Extract Constant Pos.compare_cont =>
@@ -47,12 +47,12 @@ Extract Constant Pos.compare_cont =>
Extract Constant N.add => "(+)".
-Extract Constant N.succ => "succ".
-Extract Constant N.pred => "fun n -> max 0 (n-1)".
-Extract Constant N.sub => "fun n m -> max 0 (n-m)".
+Extract Constant N.succ => "Pervasives.succ".
+Extract Constant N.pred => "fun n -> Pervasives.max 0 (n-1)".
+Extract Constant N.sub => "fun n m -> Pervasives.max 0 (n-m)".
Extract Constant N.mul => "( * )".
-Extract Constant N.min => "min".
-Extract Constant N.max => "max".
+Extract Constant N.min => "Pervasives.min".
+Extract Constant N.max => "Pervasives.max".
Extract Constant N.div => "fun a b -> if b=0 then 0 else a/b".
Extract Constant N.modulo => "fun a b -> if b=0 then a else a mod b".
Extract Constant N.compare =>
@@ -60,19 +60,19 @@ Extract Constant N.compare =>
Extract Constant Z.add => "(+)".
-Extract Constant Z.succ => "succ".
-Extract Constant Z.pred => "pred".
+Extract Constant Z.succ => "Pervasives.succ".
+Extract Constant Z.pred => "Pervasives.pred".
Extract Constant Z.sub => "(-)".
Extract Constant Z.mul => "( * )".
Extract Constant Z.opp => "(~-)".
-Extract Constant Z.abs => "abs".
-Extract Constant Z.min => "min".
-Extract Constant Z.max => "max".
+Extract Constant Z.abs => "Pervasives.abs".
+Extract Constant Z.min => "Pervasives.min".
+Extract Constant Z.max => "Pervasives.max".
Extract Constant Z.compare =>
"fun x y -> if x=y then Eq else if x<y then Lt else Gt".
Extract Constant Z.of_N => "fun p -> p".
-Extract Constant Z.abs_N => "abs".
+Extract Constant Z.abs_N => "Pervasives.abs".
(** Z.div and Z.modulo are quite complex to define in terms of (/) and (mod).
For the moment we don't even try *)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index e76c6919..0a17453c 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -130,7 +130,7 @@ let rec nb_default_params env c =
(* Enriching a signature with implicit information *)
-let sign_with_implicits r s =
+let sign_with_implicits r s nb_params =
let implicits = implicits_of_global r in
let rec add_impl i = function
| [] -> []
@@ -139,7 +139,7 @@ let sign_with_implicits r s =
if sign = Keep && List.mem i implicits then Kill Kother else sign
in sign' :: add_impl (succ i) s
in
- add_impl 1 s
+ add_impl (1+nb_params) s
(* Enriching a exception message *)
@@ -667,20 +667,23 @@ and extract_cst_app env mle mlt kn args =
let head = put_magic_if magic1 (MLglob (ConstRef kn)) in
(* Now, the extraction of the arguments. *)
let s_full = type2signature env (snd schema) in
- let s_full = sign_with_implicits (ConstRef kn) s_full in
+ let s_full = sign_with_implicits (ConstRef kn) s_full 0 in
let s = sign_no_final_keeps s_full in
let ls = List.length s in
let la = List.length args in
(* The ml arguments, already expunged from known logical ones *)
let mla = make_mlargs env mle s args metas in
let mla =
- if not magic1 then
+ if magic1 || lang () <> Ocaml then mla
+ else
try
+ (* for better optimisations later, we discard dependent args
+ of projections and replace them by fake args that will be
+ removed during final pretty-print. *)
let l,l' = list_chop (projection_arity (ConstRef kn)) mla in
if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
else mla
with _ -> mla
- else mla
in
(* For strict languages, purely logical signatures with at least
one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
@@ -726,7 +729,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
let type_cons = instantiation (nb_tvars, type_cons) in
(* Then, the usual variables [s], [ls], [la], ... *)
let s = List.map (type2sign env) types in
- let s = sign_with_implicits (ConstructRef cp) s in
+ let s = sign_with_implicits (ConstructRef cp) s params_nb in
let ls = List.length s in
let la = List.length args in
assert (la <= ls + params_nb);
@@ -805,7 +808,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
let l = List.map f oi.ip_types.(i) in
(* the corresponding signature *)
let s = List.map (type2sign env) oi.ip_types.(i) in
- let s = sign_with_implicits r s in
+ let s = sign_with_implicits r s mi.ind_nparams in
(* Extraction of the branch (in functional form). *)
let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in
(* We suppress dummy arguments according to signature. *)
@@ -876,7 +879,7 @@ let extract_std_constant env kn body typ =
let l,t' = type_decomp (expand env (var2var' t)) in
let s = List.map (type2sign env) l in
(* Check for user-declared implicit information *)
- let s = sign_with_implicits (ConstRef kn) s in
+ let s = sign_with_implicits (ConstRef kn) s 0 in
(* Decomposing the top level lambdas of [body].
If there isn't enough, it's ok, as long as remaining args
aren't to be pruned (and initial lambdas aren't to be all
@@ -923,6 +926,19 @@ let extract_std_constant env kn body typ =
in
trm, type_expunge_from_sign env s t
+(* Extracts the type of an axiom, honors the Extraction Implicit declaration. *)
+let extract_axiom env kn typ =
+ reset_meta_count ();
+ (* The short type [t] (i.e. possibly with abbreviations). *)
+ let t = snd (record_constant_type env kn (Some typ)) in
+ (* The real type [t']: without head products, expanded, *)
+ (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
+ let l,_ = type_decomp (expand env (var2var' t)) in
+ let s = List.map (type2sign env) l in
+ (* Check for user-declared implicit information *)
+ let s = sign_with_implicits (ConstRef kn) s 0 in
+ type_expunge_from_sign env s t
+
let extract_fixpoint env vkn (fi,ti,ci) =
let n = Array.length vkn in
let types = Array.make n (Tdummy Kother)
@@ -959,8 +975,8 @@ let extract_constant env kn cb =
in Dtype (r, vl, t)
in
let mk_ax () =
- let t = snd (record_constant_type env kn (Some typ)) in
- Dterm (r, MLaxiom, type_expunge env t)
+ let t = extract_axiom env kn typ in
+ Dterm (r, MLaxiom, t)
in
let mk_def c =
let e,t = extract_std_constant env kn c typ in
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 257e1c1c..bd997d2d 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -26,9 +26,9 @@ let rec msid_of_mt = function
(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
[ml_structure]. *)
-let se_iter do_decl do_spec =
+let se_iter do_decl do_spec do_mp =
let rec mt_iter = function
- | MTident _ -> ()
+ | MTident mp -> do_mp mp
| MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
| MTwith (mt,ML_With_type(idl,l,t))->
let mp_mt = msid_of_mt mt in
@@ -38,7 +38,12 @@ let se_iter do_decl do_spec =
in
let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l')) in
mt_iter mt; do_decl (Dtype(r,l,t))
- | MTwith (mt,_)->mt_iter mt
+ | MTwith (mt,ML_With_module(idl,mp))->
+ let mp_mt = msid_of_mt mt in
+ let mp_w =
+ List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl
+ in
+ mt_iter mt; do_mp mp_w; do_mp mp
| MTsig (_, sign) -> List.iter spec_iter sign
and spec_iter = function
| (_,Spec s) -> do_spec s
@@ -51,15 +56,16 @@ let se_iter do_decl do_spec =
me_iter m.ml_mod_expr; mt_iter m.ml_mod_type
| (_,SEmodtype m) -> mt_iter m
and me_iter = function
- | MEident _ -> ()
+ | MEident mp -> do_mp mp
| MEfunctor (_,mt,me) -> me_iter me; mt_iter mt
| MEapply (me,me') -> me_iter me; me_iter me'
| MEstruct (msid, sel) -> List.iter se_iter sel
in
se_iter
-let struct_iter do_decl do_spec s =
- List.iter (function (_,sel) -> List.iter (se_iter do_decl do_spec) sel) s
+let struct_iter do_decl do_spec do_mp s =
+ List.iter
+ (function (_,sel) -> List.iter (se_iter do_decl do_spec do_mp) sel) s
(*s Apply some fonctions upon all references in [ml_type], [ml_ast],
[ml_decl], [ml_spec] and [ml_structure]. *)
@@ -141,7 +147,7 @@ let decl_ast_search f = function
| _ -> ()
let struct_ast_search f s =
- try struct_iter (decl_ast_search f) (fun _ -> ()) s; false
+ try struct_iter (decl_ast_search f) (fun _ -> ()) (fun _ -> ()) s; false
with Found -> true
let rec type_search f = function
@@ -165,7 +171,9 @@ let spec_type_search f = function
| Sval (_,u) -> type_search f u
let struct_type_search f s =
- try struct_iter (decl_type_search f) (spec_type_search f) s; false
+ try
+ struct_iter (decl_type_search f) (spec_type_search f) (fun _ -> ()) s;
+ false
with Found -> true
@@ -247,34 +255,32 @@ let dfix_to_mlfix rv av i =
let c = Array.map (subst 0) av
in MLfix(i, ids, c)
+(* [optim_se] applies the [normalize] function everywhere and does the
+ inlining of code. The inlined functions are kept for the moment in
+ order to preserve the global interface, later [depcheck_se] will get
+ rid of them if possible *)
+
let rec optim_se top to_appear s = function
| [] -> []
| (l,SEdecl (Dterm (r,a,t))) :: lse ->
let a = normalize (ast_glob_subst !s a) in
let i = inline r a in
if i then s := Refmap'.add r a !s;
- if top && i && not (library ()) && not (List.mem r to_appear)
- then optim_se top to_appear s lse
- else
- let d = match optimize_fix a with
- | MLfix (0, _, [|c|]) ->
- Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|])
- | a -> Dterm (r, a, t)
- in (l,SEdecl d) :: (optim_se top to_appear s lse)
+ let d = match optimize_fix a with
+ | MLfix (0, _, [|c|]) ->
+ Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|])
+ | a -> Dterm (r, a, t)
+ in
+ (l,SEdecl d) :: (optim_se top to_appear s lse)
| (l,SEdecl (Dfix (rv,av,tv))) :: lse ->
let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in
- let all = ref true in
(* This fake body ensures that no fixpoint will be auto-inlined. *)
let fake_body = MLfix (0,[||],[||]) in
for i = 0 to Array.length rv - 1 do
if inline rv.(i) fake_body
then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s
- else all := false
done;
- if !all && top && not (library ())
- && (array_for_all (fun r -> not (List.mem r to_appear)) rv)
- then optim_se top to_appear s lse
- else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
+ (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
| (l,SEmodule m) :: lse ->
let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr}
in (l,SEmodule m) :: (optim_se top to_appear s lse)
@@ -289,7 +295,7 @@ and optim_me to_appear s = function
(* After these optimisations, some dependencies may not be needed anymore.
For non-library extraction, we recompute a minimal set of dependencies
- for first-level objects *)
+ for first-level definitions (no module pruning yet). *)
exception NoDepCheck
@@ -362,7 +368,7 @@ let rec depcheck_se = function
end
| t :: se ->
let se' = depcheck_se se in
- se_iter compute_deps_decl compute_deps_spec t;
+ se_iter compute_deps_decl compute_deps_spec add_needed_mp t;
t :: se'
let rec depcheck_struct = function
@@ -370,7 +376,7 @@ let rec depcheck_struct = function
| (mp,lse)::struc ->
let struc' = depcheck_struct struc in
let lse' = depcheck_se lse in
- (mp,lse')::struc'
+ if lse' = [] then struc' else (mp,lse')::struc'
let check_implicits = function
| MLexn s ->
@@ -389,9 +395,9 @@ let optimize_struct to_appear struc =
List.map (fun (mp,lse) -> (mp, optim_se true (fst to_appear) subst lse))
struc
in
- let opt_struc = List.filter (fun (_,lse) -> lse<>[]) opt_struc in
ignore (struct_ast_search check_implicits opt_struc);
- if library () then opt_struc
+ if library () then
+ List.filter (fun (_,lse) -> lse<>[]) opt_struc
else begin
reset_needed ();
List.iter add_needed (fst to_appear);
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index c88c6669..43b08840 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -308,13 +308,14 @@ let build_constructors_of_type ind' argl =
(Global.env ())
construct
in
- let argl =
- if argl = []
- then
+ let argl = match argl with
+ | None ->
Array.to_list
- (Array.init (cst_narg - npar) (fun _ -> mkGHole ())
+ (Array.init cst_narg (fun _ -> mkGHole ())
)
- else argl
+ | Some l ->
+ Array.to_list
+ (Array.init npar (fun _ -> mkGHole ()))@l
in
let pat_as_term =
mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
@@ -653,7 +654,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
Printer.pr_glob_constr b ++ str " in " ++
Printer.pr_glob_constr rt ++ str ". try again with a cast")
in
- let case_pats = build_constructors_of_type ind [] in
+ let case_pats = build_constructors_of_type ind None in
assert (Array.length case_pats = 2);
let brl =
list_map_i
@@ -669,12 +670,12 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
| GLetTuple(_,nal,_,b,e) ->
begin
let nal_as_glob_constr =
- List.map
+ Some (List.map
(function
Name id -> mkGVar id
| Anonymous -> mkGHole ()
)
- nal
+ nal)
in
let b_as_constr = Pretyping.Default.understand Evd.empty env b in
let b_typ = Typing.type_of env Evd.empty b_as_constr in
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 11d9a071..ab424c22 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -14,14 +14,14 @@ Delimit Scope Int_scope with I.
Module Type Int.
- Parameter int : Set.
+ Parameter t : Set.
- Parameter zero : int.
- Parameter one : int.
- Parameter plus : int -> int -> int.
- Parameter opp : int -> int.
- Parameter minus : int -> int -> int.
- Parameter mult : int -> int -> int.
+ Parameter zero : t.
+ Parameter one : t.
+ Parameter plus : t -> t -> t.
+ Parameter opp : t -> t.
+ Parameter minus : t -> t -> t.
+ Parameter mult : t -> t -> t.
Notation "0" := zero : Int_scope.
Notation "1" := one : Int_scope.
@@ -33,14 +33,14 @@ Module Type Int.
Open Scope Int_scope.
(* First, int is a ring: *)
- Axiom ring : @ring_theory int 0 1 plus mult minus opp (@eq int).
+ Axiom ring : @ring_theory t 0 1 plus mult minus opp (@eq t).
(* int should also be ordered: *)
- Parameter le : int -> int -> Prop.
- Parameter lt : int -> int -> Prop.
- Parameter ge : int -> int -> Prop.
- Parameter gt : int -> int -> Prop.
+ Parameter le : t -> t -> Prop.
+ Parameter lt : t -> t -> Prop.
+ Parameter ge : t -> t -> Prop.
+ Parameter gt : t -> t -> Prop.
Notation "x <= y" := (le x y): Int_scope.
Notation "x < y" := (lt x y) : Int_scope.
Notation "x >= y" := (ge x y) : Int_scope.
@@ -61,7 +61,7 @@ Module Type Int.
forall i j k, 0 < k -> i < j -> k*i<k*j.
(* We should have a way to decide the equality and the order*)
- Parameter compare : int -> int -> comparison.
+ Parameter compare : t -> t -> comparison.
Infix "?=" := compare (at level 70, no associativity) : Int_scope.
Axiom compare_Eq : forall i j, compare i j = Eq <-> i=j.
Axiom compare_Lt : forall i j, compare i j = Lt <-> i<j.
@@ -83,7 +83,7 @@ Module Z_as_Int <: Int.
Open Scope Z_scope.
- Definition int := Z.
+ Definition t := Z.
Definition zero := 0.
Definition one := 1.
Definition plus := Z.add.
@@ -91,7 +91,7 @@ Module Z_as_Int <: Int.
Definition minus := Z.sub.
Definition mult := Z.mul.
- Lemma ring : @ring_theory int zero one plus mult minus opp (@eq int).
+ Lemma ring : @ring_theory t zero one plus mult minus opp (@eq t).
Proof.
constructor.
exact Z.add_0_l.
@@ -138,6 +138,7 @@ End Z_as_Int.
Module IntProperties (I:Int).
Import I.
+ Local Notation int := I.t.
(* Primo, some consequences of being a ring theory... *)
@@ -827,6 +828,7 @@ Module IntOmega (I:Int).
Import I.
Module IP:=IntProperties(I).
Import IP.
+Local Notation int := I.t.
(* \subsubsection{Definition of reified integer expressions}
Terms are either:
@@ -1037,20 +1039,16 @@ Close Scope romega_scope.
Theorem eq_term_true : forall t1 t2 : term, eq_term t1 t2 = true -> t1 = t2.
Proof.
- simple induction t1; intros until t2; case t2; simpl in *;
- try (intros; discriminate; fail);
- [ intros; elim beq_true with (1 := H); trivial
- | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5;
- elim H with (1 := H4); elim H0 with (1 := H5);
- trivial
- | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5;
- elim H with (1 := H4); elim H0 with (1 := H5);
- trivial
- | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5;
- elim H with (1 := H4); elim H0 with (1 := H5);
- trivial
- | intros t21 H3; elim H with (1 := H3); trivial
- | intros; elim beq_nat_true with (1 := H); trivial ].
+ induction t1; destruct t2; simpl in *; try discriminate;
+ (rewrite andb_true_iff; intros (H1,H2)) || intros H; f_equal;
+ auto using beq_true, beq_nat_true.
+Qed.
+
+Theorem eq_term_refl : forall t0 : term, eq_term t0 t0 = true.
+Proof.
+ induction t0; simpl in *; try (apply andb_true_iff; split); trivial.
+ - now apply beq_iff.
+ - now apply beq_nat_true_iff.
Qed.
Ltac trivial_case := unfold not; intros; discriminate.
@@ -1058,31 +1056,7 @@ Ltac trivial_case := unfold not; intros; discriminate.
Theorem eq_term_false :
forall t1 t2 : term, eq_term t1 t2 = false -> t1 <> t2.
Proof.
- simple induction t1;
- [ intros z t2; case t2; try trivial_case; simpl; unfold not;
- intros; elim beq_false with (1 := H); simplify_eq H0;
- auto
- | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl;
- intros t21 t22 H3; unfold not; intro H4;
- elim andb_false_elim with (1 := H3); intros H5;
- [ elim H1 with (1 := H5); simplify_eq H4; auto
- | elim H2 with (1 := H5); simplify_eq H4; auto ]
- | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl;
- intros t21 t22 H3; unfold not; intro H4;
- elim andb_false_elim with (1 := H3); intros H5;
- [ elim H1 with (1 := H5); simplify_eq H4; auto
- | elim H2 with (1 := H5); simplify_eq H4; auto ]
- | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl;
- intros t21 t22 H3; unfold not; intro H4;
- elim andb_false_elim with (1 := H3); intros H5;
- [ elim H1 with (1 := H5); simplify_eq H4; auto
- | elim H2 with (1 := H5); simplify_eq H4; auto ]
- | intros t11 H1 t2; case t2; try trivial_case; simpl; intros t21 H3;
- unfold not; intro H4; elim H1 with (1 := H3);
- simplify_eq H4; auto
- | intros n t2; case t2; try trivial_case; simpl; unfold not;
- intros; elim beq_nat_false with (1 := H); simplify_eq H0;
- auto ].
+ intros t1 t2 H E. subst t2. now rewrite eq_term_refl in H.
Qed.
(* \subsubsection{Tactiques pour éliminer ces tests}
@@ -1919,9 +1893,9 @@ Fixpoint fusion (trace : list t_fusion) (t : term) {struct trace} : term :=
end
end.
-Theorem fusion_stable : forall t : list t_fusion, term_stable (fusion t).
+Theorem fusion_stable : forall trace : list t_fusion, term_stable (fusion trace).
Proof.
- simple induction t; simpl;
+ simple induction trace; simpl;
[ exact reduce_stable
| intros stp l H; case stp;
[ apply compose_term_stable;
@@ -2093,11 +2067,8 @@ Definition constant_not_nul (i : nat) (h : hyps) :=
Theorem constant_not_nul_valid :
forall i : nat, valid_hyps (constant_not_nul i).
Proof.
- unfold valid_hyps, constant_not_nul; intros;
- generalize (nth_valid ep e i lp); Simplify; simpl.
-
- elim_beq i1 i0; auto; simpl; intros H1 H2;
- elim H1; symmetry ; auto.
+ unfold valid_hyps, constant_not_nul; intros i ep e lp H.
+ generalize (nth_valid ep e i lp H); Simplify.
Qed.
(* \paragraph{[O_CONSTANT_NEG]} *)
@@ -2131,12 +2102,12 @@ Definition not_exact_divide (k1 k2 : int) (body : term)
end.
Theorem not_exact_divide_valid :
- forall (k1 k2 : int) (body : term) (t i : nat),
- valid_hyps (not_exact_divide k1 k2 body t i).
+ forall (k1 k2 : int) (body : term) (t0 i : nat),
+ valid_hyps (not_exact_divide k1 k2 body t0 i).
Proof.
unfold valid_hyps, not_exact_divide; intros;
generalize (nth_valid ep e i lp); Simplify.
- rewrite (scalar_norm_add_stable t e), <-H1.
+ rewrite (scalar_norm_add_stable t0 e), <-H1.
do 2 rewrite <- scalar_norm_add_stable; simpl in *; intros.
absurd (interp_term e body * k1 + k2 = 0);
[ now apply OMEGA4 | symmetry; auto ].
@@ -2509,9 +2480,9 @@ Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps :=
execute_omega cont (apply_oper_2 i1 i2 (state m s) l)
end.
-Theorem omega_valid : forall t : t_omega, valid_list_hyps (execute_omega t).
+Theorem omega_valid : forall tr : t_omega, valid_list_hyps (execute_omega tr).
Proof.
- simple induction t; simpl;
+ simple induction tr; simpl;
[ unfold valid_list_hyps; simpl; intros; left;
apply (constant_not_nul_valid n ep e lp H)
| unfold valid_list_hyps; simpl; intros; left;
@@ -2522,7 +2493,7 @@ Proof.
(apply_oper_1_valid m (divide_and_approx k1 k2 body n)
(divide_and_approx_valid k1 k2 body n) ep e lp H)
| unfold valid_list_hyps; simpl; intros; left;
- apply (not_exact_divide_valid i i0 t0 n n0 ep e lp H)
+ apply (not_exact_divide_valid _ _ _ _ _ ep e lp H)
| unfold valid_list_hyps, valid_hyps;
intros k body n t' Ht' m ep e lp H; apply Ht';
apply
@@ -2618,10 +2589,10 @@ Qed.
(* \subsubsection{Exécution de la trace} *)
Theorem execute_goal :
- forall (t : t_omega) (ep : list Prop) (env : list int) (l : hyps),
- interp_list_goal ep env (execute_omega t l) -> interp_goal ep env l.
+ forall (tr : t_omega) (ep : list Prop) (env : list int) (l : hyps),
+ interp_list_goal ep env (execute_omega tr l) -> interp_goal ep env l.
Proof.
- intros; apply (goal_valid (execute_omega t) (omega_valid t) ep env l H).
+ intros; apply (goal_valid (execute_omega tr) (omega_valid tr) ep env l H).
Qed.
@@ -2936,13 +2907,13 @@ Proof.
| intro; apply ne_left_2; assumption ]
| case p; simpl; intros; auto; generalize H; elim (t_rewrite_stable s);
simpl; intro H1;
- [ rewrite (plus_0_r_reverse (interp_term e t0)); rewrite H1;
+ [ rewrite (plus_0_r_reverse (interp_term e t1)); rewrite H1;
rewrite plus_permute; rewrite plus_opp_r;
rewrite plus_0_r; trivial
- | apply (fun a b => plus_le_reg_r a b (- interp_term e t));
+ | apply (fun a b => plus_le_reg_r a b (- interp_term e t0));
rewrite plus_opp_r; assumption
| rewrite ge_le_iff;
- apply (fun a b => plus_le_reg_r a b (- interp_term e t0));
+ apply (fun a b => plus_le_reg_r a b (- interp_term e t1));
rewrite plus_opp_r; assumption
| rewrite gt_lt_iff; apply lt_left_inv; assumption
| apply lt_left_inv; assumption
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 6a5878b3..dfcc8526 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -663,6 +663,7 @@ let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce)
let admit_obligations n =
let prg = get_prog_err n in
let obls, rem = prg.prg_obligations in
+ let obls = Array.copy obls in
Array.iteri
(fun i x ->
match x.obl_body with
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-29 10:17:23 +0000