diff options
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 23d066df58..150dad16c2 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -76,6 +76,7 @@ let mkProj (p, c) = of_kind (Proj (p, c)) let mkArrow t1 r t2 = of_kind (Prod (make_annot Anonymous r, t1, t2)) let mkArrowR t1 t2 = mkArrow t1 Sorts.Relevant t2 let mkInt i = of_kind (Int i) +let mkFloat f = of_kind (Float f) let mkRef (gr,u) = let open GlobRef in match gr with | ConstRef c -> mkConstU (c,u) @@ -334,7 +335,7 @@ let iter_with_full_binders sigma g f n c = let open Context.Rel.Declaration in match kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _) -> () + | Construct _ | Int _ | Float _) -> () | Cast (c,_,t) -> f n c; f n t | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c @@ -462,16 +463,16 @@ let test_constr_universes env sigma leq m n = if Sorts.equal s1 s2 then true else (cstrs := Set.add (UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs; - true) + true) in - let leq_sorts s1 s2 = + let leq_sorts s1 s2 = let s1 = ESorts.kind sigma s1 in let s2 = ESorts.kind sigma s2 in if Sorts.equal s1 s2 then true - else + else (cstrs := Set.add (ULe (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs; - true) + true) in let rec eq_constr' nargs m n = compare_gen kind eq_universes eq_sorts eq_constr' nargs m n in let res = @@ -495,20 +496,20 @@ let compare_head_gen_proj env sigma equ eqs eqc' nargs m n = let kind c = kind sigma c in match kind m, kind n with | Proj (p, c), App (f, args) - | App (f, args), Proj (p, c) -> + | App (f, args), Proj (p, c) -> (match kind f with - | Const (p', u) when Constant.equal (Projection.constant p) p' -> + | Const (p', u) when Constant.equal (Projection.constant p) p' -> let npars = Projection.npars p in if Array.length args == npars + 1 then eqc' 0 c args.(npars) - else false + else false | _ -> false) | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' nargs m n let eq_constr_universes_proj env sigma m n = let open UnivProblem in if m == n then Some Set.empty - else + else let cstrs = ref Set.empty in let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in let eq_sorts s1 s2 = @@ -518,7 +519,7 @@ let eq_constr_universes_proj env sigma m n = else (cstrs := Set.add (UEq (Sorts.univ_of_sort s1, Sorts.univ_of_sort s2)) !cstrs; - true) + true) in let rec eq_constr' nargs m n = m == n || compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' nargs m n |