From 1db568d3dc88d538f975377bb4d8d3eecd87872c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Aug 2017 19:05:57 +0200 Subject: Making detyping potentially lazy. The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager. --- plugins/cc/cctac.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/cc') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 5a4c52456..fca7d9851 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -442,11 +442,11 @@ let cc_tactic depth additionnal_terms = let open Glob_term in let env = Proofview.Goal.env gl in let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in - let hole = CAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in + let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in let pr_missing (c, missing) = - let c = Detyping.detype ~lax:true false [] env sigma c in + let c = Detyping.detype Detyping.Now ~lax:true false [] env sigma c in let holes = List.init missing (fun _ -> hole) in - Printer.pr_glob_constr_env env (CAst.make @@ GApp (c, holes)) + Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes)) in Feedback.msg_info (Pp.str "Goal is solvable by congruence but some arguments are missing."); -- cgit v1.2.3