aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/newring.ml418
1 files changed, 10 insertions, 8 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index aecbbfe85..be661587a 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -176,7 +176,7 @@ let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c)
let dummy_goal env =
let (gl,_,sigma) =
Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Evd.Store.empty in
- {Evd.it = gl;
+ {Evd.it = gl; Evd.eff=Declareops.no_seff;
Evd.sigma = sigma}
let exec_tactic env n f args =
@@ -679,8 +679,10 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div =
let lemma1 = constr_of params.(3) in
let lemma2 = constr_of params.(4) in
- let lemma1 = decl_constant (Id.to_string name^"_ring_lemma1") lemma1 in
- let lemma2 = decl_constant (Id.to_string name^"_ring_lemma2") lemma2 in
+ let lemma1 =
+ decl_constant (Id.to_string name^"_ring_lemma1") (Future.from_val ( lemma1,Declareops.no_seff)) in
+ let lemma2 =
+ decl_constant (Id.to_string name^"_ring_lemma2") (Future.from_val ( lemma2,Declareops.no_seff)) in
let cst_tac =
interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
let pretac =
@@ -1030,11 +1032,11 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi
match inj with
| Some thm -> mkApp(constr_of params.(8),[|thm|])
| None -> constr_of params.(7) in
- let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") lemma1 in
- let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") lemma2 in
- let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") lemma3 in
- let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") lemma4 in
- let cond_lemma = decl_constant (Id.to_string name^"_lemma5") cond_lemma in
+ let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") (Future.from_val (lemma1,Declareops.no_seff)) in
+ let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") (Future.from_val (lemma2,Declareops.no_seff)) in
+ let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") (Future.from_val (lemma3,Declareops.no_seff)) in
+ let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") (Future.from_val (lemma4,Declareops.no_seff)) in
+ let cond_lemma = decl_constant (Id.to_string name^"_lemma5") (Future.from_val (cond_lemma,Declareops.no_seff)) in
let cst_tac =
interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
let pretac =