diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index ac653c75..09ec8dda 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: evarutil.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Util open Pp @@ -1434,6 +1434,10 @@ let judge_of_new_Type () = Typeops.judge_of_type (new_univ ()) constraint on its domain and codomain. If the input constraint is an evar instantiate it with the product of 2 new evars. *) +let unlift_tycon init cur c = + if cur = 1 then None, c + else Some (init, pred cur), c + let split_tycon loc env evd tycon = let rec real_split evd c = let t = whd_betadeltaiota env evd c in @@ -1453,14 +1457,7 @@ let split_tycon loc env evd tycon = let evd', (n, dom, rng) = real_split evd c in evd', (n, mk_tycon dom, mk_tycon rng) | Some (init, cur) -> - if cur = 0 then - let evd', (x, dom, rng) = real_split evd c in - evd, (Anonymous, - Some (None, dom), - Some (None, rng)) - else - evd, (Anonymous, None, - Some (if cur = 1 then None,c else Some (init, pred cur), c))) + evd, (Anonymous, None, Some (unlift_tycon init cur c))) let valcon_of_tycon x = match x with |