diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/redexpr.ml | 4 | ||||
| -rw-r--r-- | proofs/redexpr.mli | 3 | ||||
| -rw-r--r-- | proofs/tacexpr.ml | 14 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 2 |
4 files changed, 13 insertions, 10 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 27db71755..71e7cdc21 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -154,8 +154,8 @@ let out_arg = function | ArgVar _ -> anomaly "Unevaluated or_var variable" | ArgArg x -> x -let out_with_occurrences (l,c) = - (List.map out_arg l, c) +let out_with_occurrences ((b,l),c) = + ((b,List.map out_arg l), c) let reduction_of_red_expr = function | Red internal -> diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index 68c1fd669..70db56c48 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -13,11 +13,12 @@ open Term open Closure open Rawterm open Reductionops +open Termops type red_expr = (constr, evaluable_global_reference) red_expr_gen -val out_with_occurrences : 'a with_occurrences -> int list * 'a +val out_with_occurrences : 'a with_occurrences -> occurrences * 'a val reduction_of_red_expr : red_expr -> reduction_function * cast_kind (* [true] if we should use the vm to verify the reduction *) diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index d0b015552..17961fd42 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -94,15 +94,17 @@ type 'id gsimple_clause = ('id raw_hyp_location) option [Some l] means on hypothesis belonging to l *) type 'id gclause = { onhyps : 'id raw_hyp_location list option; - onconcl : bool; - concl_occs : int or_var list } + concl_occs : bool * int or_var list } -let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]} +let nowhere = {onhyps=Some[]; concl_occs=(false,[])} let simple_clause_of = function - { onhyps = Some[scl]; onconcl = false } -> Some scl - | { onhyps = Some []; onconcl = true; concl_occs=[] } -> None - | _ -> error "not a simple clause (one hypothesis or conclusion)" +| { onhyps = Some [scl]; concl_occs = occs } when occs = no_occurrences_expr -> + Some scl +| { onhyps = Some []; concl_occs = occs } when occs = all_occurrences_expr -> + None +| _ -> + error "not a simple clause (one hypothesis or conclusion)" type multi = | Precisely of int diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 6b6305a17..2b007112f 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -79,7 +79,7 @@ val pf_nf_betaiota : goal sigma -> constr -> constr val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types val pf_reduce_to_atomic_ind : goal sigma -> types -> inductive * types val pf_compute : goal sigma -> constr -> constr -val pf_unfoldn : (int list * evaluable_global_reference) list +val pf_unfoldn : (Termops.occurrences * evaluable_global_reference) list -> goal sigma -> constr -> constr val pf_const_value : goal sigma -> constant -> constr |