diff options
| author | Yves Bertot | 2018-05-10 08:21:40 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-10 08:21:40 +0200 |
| commit | cb49f4c22261174f4c0a7f1a26fa795af8ed2155 (patch) | |
| tree | 7529019ab564566773efad00ed1c67340162e59f | |
| parent | a3f8e01c9e705fcc2d73187ebf3f26d586b47f8d (diff) | |
finished the example where type class resolution is forced
| -rw-r--r-- | tuto3/src/construction_game.ml | 6 | ||||
| -rw-r--r-- | tuto3/src/g_tuto3.ml4 | 2 |
2 files changed, 7 insertions, 1 deletions
diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml index 9a3d046cf5..0a94419e83 100644 --- a/tuto3/src/construction_game.ml +++ b/tuto3/src/construction_game.ml @@ -155,6 +155,7 @@ let example_classes n = let arg_type = EConstr.mkApp (c_even, [| c_n |]) in let env = Global.env () in let evd = Evd.from_env env in + let evd0 = evd in let evd, instance = Evarutil.new_evar env evd arg_type in let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in let _ = Feedback.msg_notice (Termops.print_constr_env env evd c_half) in @@ -163,6 +164,11 @@ let example_classes n = let proved_equality = EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), Constr.DEFAULTcast, EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in +(* This is where we force the system to compute with type classes. *) +(* Question to coq developers: why do we pass two evd arguments to + solve_remaining_evars? Is the choice of evd0 relevant here? *) + let evd = Pretyping.solve_remaining_evars + (Pretyping.default_inference_flags true) env evd evd0 in let evd, final_type = Typing.type_of env evd proved_equality in Feedback.msg_notice (Termops.print_constr_env env evd proved_equality) diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4 index 963662895a..f028880087 100644 --- a/tuto3/src/g_tuto3.ml4 +++ b/tuto3/src/g_tuto3.ml4 @@ -28,7 +28,7 @@ VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY | [ "Tuto3_3" int(n) ] -> [ example_classes n ] END -VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY +VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY | [ "Tuto3_4" int(n) ] -> [ example_canonical n ] END |