Commit b3966675 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Revert "logical symbols are not allowed in programs anymore"

This reverts commit b65dd4ae.
parent b68e35e5
...@@ -567,9 +567,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} = ...@@ -567,9 +567,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
let qualid_app loc q el = let qualid_app loc q el =
let e = try match find_prog_symbol muc q with let e = try match find_prog_symbol muc q with
| PV pv -> DEpv pv | RS rs -> DErs rs with | PV pv -> DEpv pv | RS rs -> DErs rs with
| _ -> ignore (find_lsymbol muc.muc_theory q); | _ -> DEls (find_lsymbol muc.muc_theory q) in
Loc.errorm ~loc "Symbol %a is a pure logical symbol, \
it cannot be used in a program" print_qualid q in
expr_app loc e el expr_app loc e el
in in
let qualid_app loc q el = match q with let qualid_app loc q el = match q with
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment