aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-11-06 03:11:44 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 17:23:54 +0100
commitb113f9e1ca88514cd9d94dfe90669a27689b7434 (patch)
tree7301bc9a26dc676a17067b4e27d2765129671e1e /pretyping
parentb7fd585b89ac5e0b7770f52739c33fe179f2eed8 (diff)
Recordops API using EConstr.
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/recordops.ml6
-rw-r--r--pretyping/recordops.mli2
2 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 062e4a068..f09f3221d 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -171,7 +171,7 @@ let keep_true_projections projs kinds =
let filter (p, (_, b)) = if b then Some p else None in
List.map_filter filter (List.combine projs kinds)
-let cs_pattern_of_constr sigma t =
+let cs_pattern_of_constr t =
match kind_of_term t with
App (f,vargs) ->
begin
@@ -179,7 +179,7 @@ let cs_pattern_of_constr sigma t =
with e when CErrors.noncritical e -> raise Not_found
end
| Rel n -> Default_cs, Some n, []
- | Prod (_,a,b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b) -> Prod_cs, None, [a; Termops.pop (EConstr.of_constr b)]
+ | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
| Sort s -> Sort_cs (family_of_sort s), None, []
| _ ->
begin
@@ -217,7 +217,7 @@ let compute_canonical_projections warn (con,ind) =
| Some proji_sp ->
begin
try
- let patt, n , args = cs_pattern_of_constr Evd.empty t (** FIXME *) in
+ let patt, n , args = cs_pattern_of_constr t in
((ConstRef proji_sp, patt, t, n, args) :: l)
with Not_found ->
let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 405963a9c..7c0d0ec6d 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -65,7 +65,7 @@ type obj_typ = {
o_TCOMPS : constr list } (** ordered *)
(** Return the form of the component of a canonical structure *)
-val cs_pattern_of_constr : Evd.evar_map -> constr -> cs_pattern * int option * constr list
+val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list
val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds