diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-30 17:53:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:20:30 +0100 |
| commit | 5143129baac805d3a49ac3ee9f3344c7a447634f (patch) | |
| tree | 60fd3fb22fc95474454a6a60f3a8715bf7d766d0 /plugins/cc | |
| parent | a42795cc1c2a8ed3efa9960af920ff7b16d928f0 (diff) | |
Termops API using EConstr.
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/cctac.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index b5ca2f50f..425bb2d6f 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -58,8 +58,8 @@ let rec decompose_term env sigma t= let tf=decompose_term env sigma f in let targs=Array.map (decompose_term env sigma) args in Array.fold_left (fun s t->Appli (s,t)) tf targs - | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) -> - let b = Termops.pop _b in + | Prod (_,a,_b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr _b) -> + let b = Termops.pop (EConstr.of_constr _b) in let sort_b = sf_of env sigma b in let sort_a = sf_of env sigma a in Appli(Appli(Product (sort_a,sort_b) , @@ -86,7 +86,7 @@ let rec decompose_term env sigma t= let p' = Projection.map canon_const p in (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c)) | _ -> - let t = Termops.strip_outer_cast t in + let t = Termops.strip_outer_cast sigma (EConstr.of_constr t) in if closed0 t then Symb t else raise Not_found (* decompose equality in members and type *) @@ -112,8 +112,8 @@ let rec pattern_of_constr env sigma c = (Array.map_to_list (pattern_of_constr env sigma) args) in PApp (pf,List.rev pargs), List.fold_left Int.Set.union Int.Set.empty lrels - | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) -> - let b = Termops.pop _b in + | Prod (_,a,_b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr _b) -> + let b = Termops.pop (EConstr.of_constr _b) in let pa,sa = pattern_of_constr env sigma a in let pb,sb = pattern_of_constr env sigma b in let sort_b = sf_of env sigma b in |