diff options
| -rw-r--r-- | contrib/ring/Ring_abstract.v | 4 | ||||
| -rw-r--r-- | contrib/ring/ring.ml | 13 |
2 files changed, 12 insertions, 5 deletions
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v index 7626899850..05a6f68507 100644 --- a/contrib/ring/Ring_abstract.v +++ b/contrib/ring/Ring_abstract.v @@ -100,7 +100,7 @@ Fixpoint interp_asp [p:aspolynomial] : A := | (ASPmult l r) => (Amult (interp_asp l) (interp_asp r)) end. -Local iacs_aux := Fix iacs_aux{iacs_aux [a:A; s:abstract_sum] : A := +(* Local *) Definition iacs_aux := Fix iacs_aux{iacs_aux [a:A; s:abstract_sum] : A := Cases s of | Nil_acs => a | (Cons_acs l t) => (Aplus a (iacs_aux (interp_vl Amult Aone Azero vm l) t)) @@ -384,7 +384,7 @@ Variable Aeq : A -> A -> bool. Variable vm : (varmap A). Variable T : (Ring_Theory Aplus Amult Aone Azero Aopp Aeq). -Local isacs_aux := Fix isacs_aux{isacs_aux [a:A; s:signed_sum] : A := +(* Local *) Definition isacs_aux := Fix isacs_aux{isacs_aux [a:A; s:signed_sum] : A := Cases s of | Nil_varlist => a | (Plus_varlist l t) => diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 589c1580ea..5c6ec33d5a 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -536,7 +536,14 @@ let constants_to_unfold = path_of_string "Coq.ring.Ring_normalize.interp_vl"; path_of_string "Coq.ring.Ring_abstract.interp_acs"; path_of_string "Coq.ring.Ring_abstract.interp_sacs"; - path_of_string "Coq.ring.Quote.varmap_find" ] + path_of_string "Coq.ring.Quote.varmap_find"; + (* anciennement des Local devenus Definition *) + path_of_string "Coq.ring.Ring_normalize.ics_aux"; + path_of_string "Coq.ring.Ring_normalize.ivl_aux"; + path_of_string "Coq.ring.Ring_normalize.interp_m"; + path_of_string "Coq.ring.Ring_abstract.iacs_aux"; + path_of_string "Coq.ring.Ring_abstract.isacs_aux"; + ] (* SectionPathSet.empty *) (* Unfolds the functions interp and find_btree in the term c of goal gl *) @@ -575,10 +582,10 @@ let raw_polynom th op lc gl = (tclORELSE (h_exact c'i_eq_c''i) (h_exact (mkAppA - [| build_coq_sym_eqT (); th.th_a; c'''i; ci; c'i_eq_c''i |])) + [| build_coq_sym_eqT (); th.th_a; c''i; ci; c'i_eq_c''i |])) ) (tclTHENS - (elim_type (mkAppA [| build_coq_eqT (); th.th_a; c'''i; ci |])) + (elim_type (mkAppA [| build_coq_eqT (); th.th_a; c''i; ci |])) [ tac ; h_exact c'i_eq_c''i ] |