From 3c75c1095118fe64545552e75f68b86343720361 Mon Sep 17 00:00:00 2001 From: notin Date: Tue, 20 Feb 2007 14:45:11 +0000 Subject: [PATCH] small fix to make it compile again --- helm/software/daemons/whelp/searchEngine.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/daemons/whelp/searchEngine.ml b/helm/software/daemons/whelp/searchEngine.ml index 924f69a76..2924f6eb1 100644 --- a/helm/software/daemons/whelp/searchEngine.ml +++ b/helm/software/daemons/whelp/searchEngine.ml @@ -373,7 +373,7 @@ let exec_action dbd (req: Http_types.request) outchan = | "/match" -> Whelp.match_term ~dbd term | "/instance" -> Whelp.instance ~dbd term | "/hint" -> - let status = ProofEngineTypes.initial_status term metasenv in + let status = ProofEngineTypes.initial_status term metasenv [] in let intros = PrimitiveTactics.intros_tac () in let subgoals = ProofEngineTypes.apply_tactic intros status in (match subgoals with -- 2.39.2