aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/funind/functional_principles_proofs.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index d7c627248f..45dee78311 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -1350,8 +1350,8 @@ let build_clause eqs =
(fun id -> ([],id),Tacexpr.InHyp)
eqs
);
- onconcl = false;
- concl_occs = []
+ Tacexpr.onconcl = false;
+ Tacexpr.concl_occs = []
}
let rec rewrite_eqs_in_eqs eqs =