diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-31 17:43:18 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-13 12:57:39 +0200 |
| commit | 3a0b543af4ac99b29efdebe27b1d204d044a7bf0 (patch) | |
| tree | e1f926647c686a559b045654924a50535afa25c0 /pretyping/retyping.ml | |
| parent | f3b84cf63c242623bdcccd30c536e55983971da5 (diff) | |
Evar maps contain econstrs.
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 95aa5ebef..746a68b21 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -57,8 +57,8 @@ let get_type_from_constraints env sigma t = if isEvar sigma (fst (decompose_app_vect sigma t)) then match List.map_filter (fun (pbty,env,t1,t2) -> - if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t1) then Some t2 - else if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t2) then Some t1 + if is_fconv Reduction.CONV env sigma t t1 then Some t2 + else if is_fconv Reduction.CONV env sigma t t2 then Some t1 else None) (snd (Evd.extract_all_conv_pbs sigma)) with @@ -99,7 +99,7 @@ let retype ?(polyprop=true) sigma = let rec type_of env cstr = match EConstr.kind sigma cstr with | Meta n -> - (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus) + (try strip_outer_cast sigma (Evd.meta_ftype sigma n).Evd.rebus with Not_found -> retype_error (BadMeta n)) | Rel n -> let ty = RelDecl.get_type (lookup_rel n env) in @@ -115,7 +115,7 @@ let retype ?(polyprop=true) sigma = try Inductiveops.find_rectype env sigma t with Not_found -> try - let t = EConstr.of_constr (get_type_from_constraints env sigma t) in + let t = get_type_from_constraints env sigma t in Inductiveops.find_rectype env sigma t with Not_found -> retype_error BadRecursiveType in |