diff options
| author | filliatr | 2001-02-02 08:16:59 +0000 |
|---|---|---|
| committer | filliatr | 2001-02-02 08:16:59 +0000 |
| commit | 9812ffc78f2638de53884c3e06420a24ec823ecc (patch) | |
| tree | db5f5a31af2f800fe6129ae51013e74fd4f0c392 | |
| parent | ae31dfa45cadb44106ff27dbf723abc7a8c874c1 (diff) | |
retablissement (provisoire) de l'ancien Ring a cause d'une explosion en temps sur les preuves de Nijmegen + correction partielle de la simplification par Ring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1312 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/ring/ring.ml | 23 |
1 files changed, 17 insertions, 6 deletions
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index b9cce1e29d..663390c0d4 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -520,12 +520,12 @@ module SectionPathSet = SectionPathSet; peut-être faudra-t-il la déplacer dans Closure *) let constants_to_unfold = (* List.fold_right SectionPathSet.add *) - [ path_of_string "#Ring_normalize#interp_cs.cci"; - path_of_string "#Ring_normalize#interp_var.cci"; - path_of_string "#Ring_normalize#interp_vl.cci"; - path_of_string "#Ring_abstract#interp_acs.cci"; - path_of_string "#Ring_abstract#interp_sacs.cci"; - path_of_string "#Quote#varmap_find.cci" ] + [ path_of_string "Coq.ring.Ring_normalize.interp_cs"; + path_of_string "Coq.ring.Ring_normalize.interp_var"; + 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" ] (* SectionPathSet.empty *) (* Unfolds the functions interp and find_btree in the term c of goal gl *) @@ -557,6 +557,7 @@ let raw_polynom th op lc gl = let polynom_tac = List.fold_right2 (fun ci (c'i, c''i, c'i_eq_c''i) tac -> +(*** let c'''i = pf_nf gl c''i in if pf_conv_x gl c'''i ci then tac (* convertible terms *) else @@ -574,6 +575,16 @@ let raw_polynom th op lc gl = ) ) ) lc ltriplets polynom_unfold_tac +***) + tclTHENS + (elim_type (mkAppA [| Lazy.force coq_eqT; th.th_a; c'i; ci |])) + [ tclTHENS + (elim_type + (mkAppA [| Lazy.force coq_eqT; th.th_a; c''i; c'i |])) + [ tac; + h_exact c'i_eq_c''i ]; + h_reflexivity]) + lc ltriplets polynom_unfold_tac in polynom_tac gl |