diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-24 17:15:28 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-27 18:49:46 +0200 |
| commit | 0ca486fad19fc3da5160148ee4bce72b1e39ded3 (patch) | |
| tree | 64339dfab2cb1b8c1056d52f87299a333f4aec40 /plugins/cc | |
| parent | 18dca1c4310b66e012bea9a47c481676190baa5e (diff) | |
Congruence: Fixing a bug with native projections.
There is a code to turn constants denoting projections into proper
primitive projections, but it did not drop parameters.
The code seems anyway redundant with an "expand_projections" which is
already present in Cctac.decompose_term. After removal of this code,
the two calls to congruence added to cc.v work.
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 22 |
1 files changed, 2 insertions, 20 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 39348a3e7..8e53a044d 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -427,7 +427,7 @@ let cc_product s1 s2 = mkLambda(_B_,mkSort(s2),_body_)) let rec constr_of_term = function - Symb s-> applist_projection s [] + Symb s-> s | Product(s1,s2) -> cc_product s1 s2 | Eps id -> mkVar id | Constructor cinfo -> mkConstructU cinfo.ci_constr @@ -435,25 +435,7 @@ let rec constr_of_term = function make_app [(constr_of_term s2)] s1 and make_app l=function Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1 - | other -> - applist_proj other l -and applist_proj c l = - match c with - | Symb s -> applist_projection s l - | _ -> Term.applistc (constr_of_term c) l -and applist_projection c l = - match Constr.kind c with - | Const c when Environ.is_projection (fst c) (Global.env()) -> - let p = Projection.make (fst c) false in - (match l with - | [] -> (* Expand the projection *) - let ty = Typeops.type_of_constant_in (Global.env ()) c in (* FIXME constraints *) - let pb = Environ.lookup_projection p (Global.env()) in - let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in - Term.it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx - | hd :: tl -> - Term.applistc (mkProj (p, hd)) tl) - | _ -> Term.applistc c l + | other -> Term.applist (constr_of_term other,l) let rec canonize_name sigma c = let c = EConstr.Unsafe.to_constr c in |