diff options
| author | herbelin | 2000-10-25 15:08:23 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-25 15:08:23 +0000 |
| commit | 5925fff753b14f2e5f263c531eed05255c6513be (patch) | |
| tree | bf9c696625e69833787dee15e65ac494e9917417 | |
| parent | 57570e4dfa9588f51c5148932849a847cb30accb (diff) | |
Manquait le cas Constr de dyn_polynom
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@761 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/ring/ring.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index d2064380b2..cac953b38f 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -77,7 +77,7 @@ let coq_interp_asp = lazy (constant "#Ring_abstract#interp_asp.cci" "interp_asp") let coq_interp_ap = lazy (constant "#Ring_abstract#interp_ap.cci" "interp_ap") -let coq_interp_acs = + let coq_interp_acs = lazy (constant "#Ring_abstract#interp_acs.cci" "interp_acs") let coq_interp_sacs = lazy (constant "#Ring_abstract#interp_sacs.cci" "interp_sacs") @@ -585,8 +585,7 @@ let guess_eq_tac th = th.th_a; th.th_a; th.th_a; th.th_mult |])))))) -let polynom lcom gl = - let lc = (List.map (pf_interp_constr gl) lcom) in +let polynom lc gl = match lc with (* If no argument is given, try to recognize either an equality or a declared relation with arguments c1 ... cn, @@ -617,12 +616,13 @@ let polynom lcom gl = [< 'sTR" All terms must have the same type" >]; (tclTHEN (raw_polynom th None lc) polynom_unfold_tac) gl -let dyn_polynom ltacargs = +let dyn_polynom ltacargs gl = polynom (List.map (function - | Command c -> c + | Command c -> pf_interp_constr gl c + | Constr c -> c | _ -> anomaly "dyn_polynom") - ltacargs) + ltacargs) gl let v_polynom = add_tactic "Ring" dyn_polynom |