diff options
| author | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
| commit | c70412ec8b0bb34b7a5607c07d34607a147d834c (patch) | |
| tree | 0cc6cd76a8f70dfd2f5b55b0db96db4de2ff07a2 /pretyping/typing.ml | |
| parent | 720ee2730684cc289cef588482323d177e0bea59 (diff) | |
| parent | 191e253d1d1ebd6c76c63b3d83f4228e46196a6e (diff) | |
Merge PR #6914: Primitive integers
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index b5729d7574..e8d935fcbb 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -306,6 +306,9 @@ let type_of_constructor env sigma ((ind,_ as ctor),u) = let sigma = Evd.add_constraints sigma csts in sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstructRef ctor))) +let judge_of_int env v = + Termops.on_judgment EConstr.of_constr (judge_of_int env v) + (* cstr must be in n.f. w.r.t. evars and execute returns a judgement where both the term and type are in n.f. *) let rec execute env sigma cstr = @@ -408,6 +411,9 @@ let rec execute env sigma cstr = let sigma, tj = type_judgment env sigma tj in judge_of_cast env sigma cj k tj + | Int i -> + sigma, judge_of_int env i + and execute_recdef env sigma (names,lar,vdef) = let sigma, larj = execute_array env sigma lar in let sigma, lara = Array.fold_left_map (assumption_of_judgment env) sigma larj in |