diff options
| author | Maxime Dénès | 2017-09-07 12:44:47 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-07 12:44:47 +0200 |
| commit | 084ef41c98d52078f85831c940d0a073a4ccdb7a (patch) | |
| tree | f1808d72e562f0dd674759f2f447f44cd5da9aad /plugins/funind/recdef.ml | |
| parent | 276f08cb053eed175478c4c9359e61fb949742ba (diff) | |
| parent | 1db568d3dc88d538f975377bb4d8d3eecd87872c (diff) | |
Merge PR #914: Making the detyper lazy
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index d3eccb58d7..41a10cba3c 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -190,15 +190,15 @@ let (value_f:Term.constr list -> global_reference -> Term.constr) = in let env = Environ.push_rel_context context (Global.env ()) in let glob_body = - CAst.make @@ + DAst.make @@ GCases (RegularStyle,None, - [CAst.make @@ GApp(CAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> CAst.make @@ GVar x_id) rev_x_id_l), + [DAst.make @@ GApp(DAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> DAst.make @@ GVar x_id) rev_x_id_l), (Anonymous,None)], - [Loc.tag ([v_id], [CAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), - [CAst.make @@ PatVar(Name v_id); CAst.make @@ PatVar Anonymous], + [Loc.tag ([v_id], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), + [DAst.make @@ PatVar(Name v_id); DAst.make @@ PatVar Anonymous], Anonymous)], - CAst.make @@ GVar v_id)]) + DAst.make @@ GVar v_id)]) in let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in it_mkLambda_or_LetIn body context |