diff options
| author | Yves Bertot | 2018-05-30 15:25:26 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-30 15:25:26 +0200 |
| commit | 46f908ab5a03998fa96c1a599b44e6e2b3fd9a10 (patch) | |
| tree | c6fd9f086ab0f4d2219766c55571794e35f627c7 | |
| parent | 35b4f622a118cccf5e8dd961dd75b31c3ea9e5fd (diff) | |
this version has no warnings when compiling
| -rw-r--r-- | tuto3/src/construction_game.ml | 5 | ||||
| -rw-r--r-- | tuto3/src/construction_game.mli | 1 |
2 files changed, 3 insertions, 3 deletions
diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml index c893952d6a..1bbfc70cb5 100644 --- a/tuto3/src/construction_game.ml +++ b/tuto3/src/construction_game.ml @@ -184,7 +184,6 @@ let example_canonical n = let c_n = mk_nat n in (* terms for "nat", "eq", "S_ev", "eq_refl", "C" *) let c_N = c_N () in - let c_Q = c_Q () in let c_F = c_F () in let c_R = c_R () in let c_C = c_C () in @@ -205,8 +204,8 @@ let example_canonical n = let evd, final_type = Typing.type_of env evd test_term in (* The computed type has two parameters, the second one is the proof. *) let value = match EConstr.kind evd final_type with - | App(_, [| _; the_half |]) -> the_half - | _ -> failwith "expecting the whole type to be ""cmp _ the_half""" in + | Constr.App(_, [| _; the_half |]) -> the_half + | _ -> failwith "expecting the whole type to be \"cmp _ the_half\"" in let _ = Feedback.msg_notice (Termops.print_constr_env env evd value) in (* I wish for a nicer way to get the value of ev2 in the evar_map *) let prf_struct = EConstr.of_constr (EConstr.to_constr evd ev2) in diff --git a/tuto3/src/construction_game.mli b/tuto3/src/construction_game.mli index 302aec1de9..1832ed6630 100644 --- a/tuto3/src/construction_game.mli +++ b/tuto3/src/construction_game.mli @@ -1,3 +1,4 @@ +val dangling_identity : Environ.env -> Evd.evar_map -> Evd.evar_map * EConstr.t val example_sort_app_lambda : unit -> unit val example_classes : int -> unit val example_canonical : int -> unit |